1 /-
2 Copyright (c) 2019 Abhimanyu Pallavi Sudhir. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Abhimanyu Pallavi Sudhir
5 Construction of the hyperreal numbers as an ultraproduct of real sequences.
6 -/
7
8 import data.real.basic algebra.field order.filter.filter_product analysis.specific_limits
src └─────────────┘ └───────────┘ └─────────────────────────┘ └──────────────────────┘
9
10 open filter filter.filter_product
11 open_locale topological_space classical
12
13 /-- Hyperreal numbers on the ultrafilter extending the cofinite filter -/
14 @[reducible] def hyperreal := filter.filterprod ℝ (@hyperfilter ℕ)
doc └───────┘
15
16 namespace hyperreal
17
18 notation `ℝ*` := hyperreal
19
20 private def U : is_ultrafilter (@hyperfilter ℕ) := is_ultrafilter_hyperfilter
21 noncomputable instance : discrete_linear_ordered_field ℝ* :=
id └───────────────────────────┘ └┘
src └───────────────────────────┘ └┘
typ └───────────────────────────┘ └┘
doc └┘
22 filter_product.discrete_linear_ordered_field U
id └──────────────────────────────────────────┘ ┴
src └──────────────────────────────────────────┘ ┴
typ └──────────────────────────────────────────┘ ┴
doc └──────────────────────────────────────────┘
23
24 /-- A sample infinitesimal hyperreal-/
25 noncomputable def epsilon : ℝ* := of_seq (λ n, n⁻¹)
id └┘ └────┘ ┴ ┴└┘
src └┘ └────┘ └┘
typ └┘ └────┘ ┴ ┴└┘
doc └┘
26
27 /-- A sample infinite hyperreal-/
28 noncomputable def omega : ℝ* := of_seq (λ n, n)
id └┘ └────┘ ┴ ┴
src └┘ └────┘
typ └┘ └────┘ ┴ ┴
doc └┘
29
30 localized "notation `ε` := hyperreal.epsilon" in hyperreal
31 localized "notation `ω` := hyperreal.omega" in hyperreal
32
33 lemma epsilon_eq_inv_omega : ε = ω⁻¹ := rfl
id ┴ ┴ ┴└┘ └─┘
src ┴ ┴ ┴└┘ └─┘
typ ┴ ┴ ┴└┘ └─┘
doc ┴ ┴
34
35 lemma inv_epsilon_eq_omega : ε⁻¹ = ω := inv_inv' ω
id ┴└┘ ┴ ┴ └──────┘ ┴
src ┴└┘ ┴ ┴ └──────┘ ┴
typ ┴└┘ ┴ ┴ └──────┘ ┴
doc ┴ ┴ ┴
36
37 lemma epsilon_pos : 0 < ε :=
id ┴ ┴
src ┴ ┴
typ ┴ ┴
doc ┴
38 suffices ∀ᶠ i in hyperfilter, (0 : ℝ) < (i : ℕ)⁻¹, by rwa lt_def U,
id └┘ ┴ └┘ └─────────┘┴ ┴ ┴ ┴ ┴ └┘ └────┘ ┴
src └┘ └┘ └─────────┘┴ ┴ ┴ ┴ └┘ └──┘└────┘┴┴
typ └┘ ┴ └┘ └─────────┘┴ ┴ ┴ ┴ ┴ └┘ └──┘└────┘┴┴
doc └┘ └┘ ┴ └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st └───────────┘
39 have h0' : {n : ℕ | ¬ n > 0} = {0} :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
40 by simp only [not_lt, (set.set_of_eq_eq_singleton).symm]; ext; exact nat.le_zero_iff,
id └────┘ └────────────────────────┘ └─────────────┘
src └─────────┘└────┘└┘ └────────────────────────┘└─────┘ └─┘ └────┘└─────────────┘
typ └─────────┘└────┘└┘ └────────────────────────┘└─────┘ └─┘ └────┘└─────────────┘
doc └─────────┘ └┘ └─────┘ └─┘ └────┘
txt └─────────┘ └┘ └─────┘ └─┘ └────┘
par └─────────┘ └┘ └─────┘ └─┘ └────┘
pid ┴└──┘└┘ └┘ └─────┘ ┴
st └────────────────────────────────────────────────────────────────────────────────┘
41 begin
st └─────
42 simp only [inv_pos', nat.cast_pos],
id └──────┘ └──────────┘
src └─────────┘└──────┘└┘└──────────┘┴
typ └─────────┘└──────┘└┘└──────────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ───────────────────────────────────┘└─
43 exact mem_hyperfilter_of_finite_compl (by convert set.finite_singleton _),
id └─────────────────────────────┘ └──────────────────┘
src └────┘└─────────────────────────────┘┴ ┴└──────┘└──────────────────┘└┘┴
typ └────┘└─────────────────────────────┘┴ ┴└──────┘└──────────────────┘└┘┴
doc └────┘ ┴ ┴└──────┘ └┘┴
txt └────┘ ┴ ┴└──────┘ └┘┴
par └────┘ ┴ ┴└──────┘ └┘┴
pid ┴ ┴ └───────┘ └─┘
st ──────────────────────────────────────────┘└─────────────────────────────┘┴└─
44 end
st ──┘
45
46 lemma epsilon_ne_zero : ε ≠ 0 := ne_of_gt epsilon_pos
id ┴ ┴ └──────┘ └─────────┘
src ┴ ┴ └──────┘ └─────────┘
typ ┴ ┴ └──────┘ └─────────┘
doc ┴
47
48 lemma omega_pos : 0 < ω := by rw ←inv_epsilon_eq_omega; exact inv_pos epsilon_pos
id ┴ ┴ └──────────────────┘ └─────┘ └─────────┘
src ┴ ┴ └──┘└──────────────────┘ └────┘└─────┘┴└─────────┘└
typ ┴ ┴ └──┘└──────────────────┘ └────┘└─────┘┴└─────────┘└
doc ┴ └──┘ └────┘ ┴ └
txt └──┘ └────┘ ┴ └
par └──┘ └────┘ ┴ └
pid └┘ ┴ ┴ └
st └────────────────────────────────────────────────────
49
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
50 lemma omega_ne_zero : ω ≠ 0 := ne_of_gt omega_pos
id ┴ ┴ └──────┘ └───────┘
src ┴ ┴ └──────┘ └───────┘
typ ┴ ┴ └──────┘ └───────┘
doc ┴
51
52 theorem epsilon_mul_omega : ε * ω = 1 := @inv_mul_cancel _ _ ω omega_ne_zero
id ┴ ┴ ┴ ┴ └────────────┘ ┴ └───────────┘
src ┴ ┴ ┴ ┴ └────────────┘ ┴ └───────────┘
typ ┴ ┴ ┴ ┴ └────────────┘ ┴ └───────────┘
doc ┴ ┴ ┴
53
54 lemma lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
id ┴ ┴ └─────┘ ┴ └────┘ ┴
src ┴ ┴ └─────┘ └────┘ ┴
typ ┴ ┴ └─────┘ ┴ └────┘ ┴
doc └─────┘ └────┘ ┴
55 ∀ {r : ℝ}, r > 0 → of_seq f < (r : ℝ*) :=
id ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └┘
src ┴ ┴ └────┘ ┴ └┘
typ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └┘
doc └┘
56 begin
st └─────
57 simp only [metric.tendsto_at_top, dist_zero_right, norm, lt_def U] at hf ⊢,
id └───────────────────┘ └─────────────┘ └────┘ ┴
src └─────────┘└───────────────────┘└┘└─────────────┘└┘ └┘└────┘┴┴└───────┘
typ └─────────┘└───────────────────┘└┘└─────────────┘└┘ └┘└────┘┴┴└───────┘
doc └─────────┘ └┘ └┘ └┘ ┴ └───────┘
txt └─────────┘ └┘ └┘ └┘ ┴ └───────┘
par └─────────┘ └┘ └┘ └┘ ┴ └───────┘
pid ┴└──┘└┘ └┘ └┘ └┘ ┴ ┴┴└─────┘
st ───────────────────────────────────────────────────────────────────────────┘└─
58 intros r hr, cases hf r hr with N hf',
id └┘ ┴ └┘
src └─────────┘ └────┘ ┴ ┴ └─────────┘
typ └─────────┘ └────┘└┘┴┴┴└┘└─────────┘
doc └─────────┘ └────┘ ┴ ┴ └─────────┘
txt └─────────┘ └────┘ ┴ ┴ └─────────┘
par └─────────┘ └────┘ ┴ ┴ └─────────┘
pid └───┘ ┴ ┴ ┴ └─────────┘
st ────────────┘└────────────────────────┘└─
59 have hs : -{i : ℕ | f i < r} ⊆ {i : ℕ | i ≤ N} :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘┴ └──┘ └─┘ ┴ ┴┴┴ └┘┴┴┴└──┘ └─┘ ┴┴┴ └────
typ └────────┘┴ └──┘ └─┘┴┴ ┴┴┴┴└┘┴┴┴└──┘ └─┘ ┴┴┴┴└────
doc └────────┘ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ ┴ ┴ └────
txt └────────┘ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ ┴ ┴ └────
par └────────┘ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ ┴ ┴ └────
pid └─────┘└─┘ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ ┴ ┴ ┴└───
st ────────────────────────────────────────────────────
60 λ i hi1, le_of_lt (by simp only [lt_iff_not_ge];
id └──────┘ └───────────┘
src ───┘ └──────┘└──────┘┴ ┴└─────────┘└───────────┘┴└─
typ ───┘ └──────┘└──────┘┴ ┴└─────────┘└───────────┘┴└─
doc ───┘ └──────┘ ┴ ┴└─────────┘ ┴└─
txt ───┘ └──────┘ ┴ ┴└─────────┘ ┴└─
par ───┘ └──────┘ ┴ ┴└─────────┘ ┴└─
pid ───┘ └──────┘ ┴ └──────────┘ └──
st ────────────────────────┘└───────────────────────────
61 exact λ hi2, hi1 (lt_of_le_of_lt (le_abs_self _) (hf' i hi2)) : i < N),
id └─┘ └────────────┘ └─────────┘ └─┘ ┴ ┴
src ───┘└────┘ └────┘ ┴ └────────────┘┴ └─────────┘└──┘ ┴ ┴ └─┘└┘ ┴ ┴ ┴
typ ───┘└────┘ └────┘└─┘┴ └────────────┘┴ └─────────┘└──┘ └─┘┴┴┴ └─┘└┘ ┴ ┴┴┴
doc ───┘└────┘ └────┘ ┴ ┴ └──┘ ┴ ┴ └─┘└┘ ┴ ┴ ┴
txt ───┘└────┘ └────┘ ┴ ┴ └──┘ ┴ ┴ └─┘└┘ ┴ ┴ ┴
par ───┘└────┘ └────┘ ┴ ┴ └──┘ ┴ ┴ └─┘└┘ ┴ ┴ ┴
pid ─────────┘ └────┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────┘└──────┘└─
62 exact mem_hyperfilter_of_finite_compl
id └─────────────────────────────┘
src └────┘└─────────────────────────────┘└
typ └────┘└─────────────────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ────────────────────────────────────────
63 (set.finite_subset (set.finite_le_nat N) hs)
id └───────────────┘ └───────────────┘ ┴ └┘
src ───┘ └───────────────┘┴ └───────────────┘┴ └┘ └┘
typ ───┘ └───────────────┘┴ └───────────────┘┴┴└┘└┘└┘
doc ───┘ ┴ ┴ └┘ └┘
txt ───┘ ┴ ┴ └┘ └┘
par ───┘ ┴ ┴ └┘ └┘
pid ───┘ ┴ ┴ └┘ ┴┴
st ────────────────────────────────────────────────┘
64 end
st └─┘
65
66 lemma neg_lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
id ┴ ┴ └─────┘ ┴ └────┘ ┴
src ┴ ┴ └─────┘ └────┘ ┴
typ ┴ ┴ └─────┘ ┴ └────┘ ┴
doc └─────┘ └────┘ ┴
67 ∀ {r : ℝ}, r > 0 → (-r : ℝ*) < of_seq f :=
id ┴ ┴ ┴ ┴┴ └┘ ┴ └────┘ ┴
src ┴ ┴ ┴ └┘ ┴ └────┘
typ ┴ ┴ ┴ ┴┴ └┘ ┴ └────┘ ┴
doc └┘
68 λ r hr, have hg : _ := hf.neg,
id ┴ └┘ └┘└──┘
src └──┘
typ ┴ └┘ └┘└──┘
69 neg_lt_of_neg_lt (by rw [neg_zero] at hg; exact lt_of_tendsto_zero_of_pos hg hr)
id └──────────────┘ └──────┘ └───────────────────────┘ └┘ └┘
src └──────────────┘ └──┘└──────┘└─────┘ └────┘└───────────────────────┘┴ ┴
typ └──────────────┘ └──┘└──────┘└─────┘ └────┘└───────────────────────┘┴└┘┴└┘
doc └──┘ └─────┘ └────┘ ┴ ┴
txt └──┘ └─────┘ └────┘ ┴ ┴
par └──┘ └─────┘ └────┘ ┴ ┴
pid └┘ ┴└────┘ ┴ ┴ ┴
st └───────────┘┴└───────────────────────────────────────────┘
70
71 lemma gt_of_tendsto_zero_of_neg {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
id ┴ ┴ └─────┘ ┴ └────┘ ┴
src ┴ ┴ └─────┘ └────┘ ┴
typ ┴ ┴ └─────┘ ┴ └────┘ ┴
doc └─────┘ └────┘ ┴
72 ∀ {r : ℝ}, r < 0 → (r : ℝ*) < of_seq f :=
id ┴ ┴ ┴ ┴ └┘ ┴ └────┘ ┴
src ┴ ┴ └┘ ┴ └────┘
typ ┴ ┴ ┴ ┴ └┘ ┴ └────┘ ┴
doc └┘
73 λ r hr, by rw [←of_eq_coe, ←neg_neg r, of_neg];
id ┴ └┘ └───────┘ └─────┘ ┴ └────┘
src └───┘└───────┘└─┘└─────┘┴ └┘└────┘┴
typ ┴ └┘ └───┘└───────┘└─┘└─────┘┴┴└┘└────┘┴
doc └───┘ └─┘ ┴ └┘ ┴
txt └───┘ └─┘ ┴ └┘ ┴
par └───┘ └─┘ ┴ └┘ ┴
pid └─┘ └─┘ ┴ └┘ ┴
st └─────────────┘└──────────┘└──────┘┴└─
74 exact neg_lt_of_tendsto_zero_of_pos hf (neg_pos.mpr hr)
id └───────────────────────────┘ └┘ └─────────┘ └┘
src └────┘└───────────────────────────┘┴ ┴ └─────────┘┴ └─
typ └────┘└───────────────────────────┘┴└┘┴ └─────────┘┴└┘└─
doc └────┘ ┴ ┴ ┴ └─
txt └────┘ ┴ ┴ ┴ └─
par └────┘ ┴ ┴ ┴ └─
pid ┴ ┴ ┴ ┴ ┴└
st ────────────────────────────────────────────────────────
75
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
76 lemma epsilon_lt_pos (x : ℝ) : x > 0 → ε < of x :=
id ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc ┴ └┘
77 lt_of_tendsto_zero_of_pos tendsto_inverse_at_top_nhds_0_nat
id └───────────────────────┘ └───────────────────────────────┘
src └───────────────────────┘ └───────────────────────────────┘
typ └───────────────────────┘ └───────────────────────────────┘
78
79 /-- Standard part predicate -/
80 def is_st (x : ℝ*) (r : ℝ) := ∀ δ : ℝ, δ > 0 → (r - δ : ℝ*) < x ∧ x < r + δ
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘
81
82 /-- Standard part function: like a "round" to ℝ instead of ℤ -/
83 noncomputable def st : ℝ* → ℝ :=
id └┘ ┴
src └┘ ┴
typ └┘ ┴
doc └┘
84 λ x, if h : ∃ r, is_st x r then classical.some h else 0
id ┴ └┘ ┴ ┴┴ └───┘ ┴ ┴ └────────────┘ ┴ ┴
src └┘ ┴ ┴ └───┘ └────────────┘ ┴
typ ┴ └┘ ┴ ┴┴ └───┘ ┴ ┴ └────────────┘ ┴ ┴
doc └───┘
85
86 /-- A hyperreal number is infinitesimal if its standard part is 0 -/
87 def infinitesimal (x : ℝ*) := is_st x 0
id └┘ └───┘ ┴
src └┘ └───┘
typ └┘ └───┘ ┴
doc └┘ └───┘
88
89 /-- A hyperreal number is positive infinite if it is larger than all real numbers -/
90 def infinite_pos (x : ℝ*) := ∀ r : ℝ, x > r
id └┘ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴
doc └┘
91
92 /-- A hyperreal number is negative infinite if it is smaller than all real numbers -/
93 def infinite_neg (x : ℝ*) := ∀ r : ℝ, x < r
id └┘ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴
doc └┘
94
95 /-- A hyperreal number is infinite if it is infinite positive or infinite negative -/
96 def infinite (x : ℝ*) := infinite_pos x ∨ infinite_neg x
id └┘ └──────────┘ ┴ ┴ └──────────┘ ┴
src └┘ └──────────┘ ┴ └──────────┘
typ └┘ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └┘ └──────────┘ └──────────┘
97
98 -- SOME FACTS ABOUT ST
99
100 private lemma is_st_unique' (x : ℝ*) (r s : ℝ) (hr : is_st x r) (hs : is_st x s) (hrs : r < s) :
id └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └───┘ └───┘ ┴
typ └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └┘ └───┘ └───┘
101 false :=
id └───┘
src └───┘
typ └───┘
102 have hrs' : _ := half_pos $ sub_pos_of_lt hrs,
id └──────┘ └───────────┘ └─┘
src └──────┘ └───────────┘
typ └──────┘ └───────────┘ └─┘
103 have hr' : _ := (hr _ hrs').2,
id └┘ └──┘ ┴
src ┴
typ └┘ └──┘ ┴
104 have hs' : _ := (hs _ hrs').1,
id └┘ └──┘ ┴
src ┴
typ └┘ └──┘ ┴
105 have h : s + -((s - r) / 2) = r + (s - r) / 2 := by linarith,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st ┴ └───────┘
106 by simp only [(of_eq_coe _).symm, sub_eq_add_neg (of s),
id └───────┘ └────────────┘ └┘ ┴
src └─────────┘ └───────┘└────────┘└────────────┘┴ └┘┴ └──
typ └─────────┘ └───────┘└────────┘└────────────┘┴ └┘┴┴└──
doc └─────────┘ └────────┘ ┴ └┘┴ └──
txt └─────────┘ └────────┘ ┴ ┴ └──
par └─────────┘ └────────┘ ┴ ┴ └──
pid ┴└──┘└┘ └────────┘ ┴ ┴ └──
st └──────────────────────────────────────────────────────
107 (of_neg _).symm, (of_add _ _).symm, h] at hr' hs';
id └────┘ └────┘ ┴
src ───┘ └────┘└────────┘ └────┘└──────────┘ └──────────┘
typ ───┘ └────┘└────────┘ └────┘└──────────┘┴└──────────┘
doc ───┘ └────────┘ └──────────┘ └──────────┘
txt ───┘ └────────┘ └──────────┘ └──────────┘
par ───┘ └────────┘ └──────────┘ └──────────┘
pid ───┘ └────────┘ └──────────┘ ┴┴└────────┘
st ───────────────────────────────────────────────────────
108 exact not_lt_of_lt hs' hr'
id └──────────┘ └─┘ └─┘
src └────┘└──────────┘┴ ┴ └
typ └────┘└──────────┘┴└─┘┴└─┘└
doc └────┘ ┴ ┴ └
txt └────┘ ┴ ┴ └
par └────┘ ┴ ┴ └
pid ┴ ┴ ┴ └
st ─────────────────────────────
109
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
110 theorem is_st_unique {x : ℝ*} {r s : ℝ} (hr : is_st x r) (hs : is_st x s) : r = s :=
id └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └───┘ └───┘ ┴
typ └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └┘ └───┘ └───┘
111 begin
st └─────
112 rcases lt_trichotomy r s with h | h | h,
id └───────────┘ ┴ ┴
src └─────┘└───────────┘┴ ┴ └─────────────┘
typ └─────┘└───────────┘┴┴┴┴└─────────────┘
doc └─────┘ ┴ ┴ └─────────────┘
txt └─────┘ ┴ ┴ └─────────────┘
par └─────┘ ┴ ┴ └─────────────┘
pid ┴ ┴ ┴ └─────────────┘
st ────────────────────────────────────────┘└─
113 { exact false.elim (is_st_unique' x r s hr hs h) },
id └────────┘ └───────────┘ ┴ ┴ ┴ └┘ └┘ ┴
src └────┘└────────┘┴ └───────────┘┴ ┴ ┴ ┴ ┴ ┴ └┘
typ └────┘└────────┘┴ └───────────┘┴┴┴┴┴┴┴└┘┴└┘┴┴└┘
doc └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st ───┘└─────────────────────────────────────────────┘└┘└
114 { exact h },
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└──────┘└┘└
115 { exact false.elim (is_st_unique' x s r hs hr h) }
id └────────┘ └───────────┘ ┴ ┴ ┴ └┘ └┘ ┴
src └────┘└────────┘┴ └───────────┘┴ ┴ ┴ ┴ ┴ ┴ └┘
typ └────┘└────────┘┴ └───────────┘┴┴┴┴┴┴┴└┘┴└┘┴┴└┘
doc └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────┘└─
116 end
st ──┘
117
118 theorem not_infinite_of_exists_st {x : ℝ*} : (∃ r : ℝ, is_st x r) → ¬ infinite x :=
id └┘ ┴ ┴┴ └───┘ ┴ ┴ ┴ └──────┘ ┴
src └┘ ┴ ┴┴ └───┘ ┴ └──────┘
typ └┘ ┴ ┴┴ └───┘ ┴ ┴ ┴ └──────┘ ┴
doc └┘ └───┘ └──────┘
119 λ he hi, Exists.dcases_on he $ λ r hr, hi.elim
id └┘ └┘ └──────────────┘ └┘ ┴ └┘ └┘└───┘
src └──────────────┘ └───┘
typ └┘ └┘ └──────────────┘ └┘ ┴ └┘ └┘└───┘
120 (λ hip, not_lt_of_lt (hr 2 two_pos).2 (hip $ r + 2))
id └─┘ └──────────┘ └┘ └─────┘ ┴ └─┘ ┴ ┴
src └──────────┘ └─────┘ ┴ ┴
typ └─┘ └──────────┘ └┘ └─────┘ ┴ └─┘ ┴ ┴
121 (λ hin, not_lt_of_lt (hr 2 two_pos).1 (hin $ r - 2))
id └─┘ └──────────┘ └┘ └─────┘ ┴ └─┘ ┴ ┴
src └──────────┘ └─────┘ ┴ ┴
typ └─┘ └──────────┘ └┘ └─────┘ ┴ └─┘ ┴ ┴
122
123 theorem is_st_Sup {x : ℝ*} (hni : ¬ infinite x) : is_st x (real.Sup {y : ℝ | of y < x}) :=
id └┘ ┴ └──────┘ ┴ └───┘ ┴ └──────┘ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ ┴ └──────┘ └───┘ └──────┘ ┴ ┴ └┘ ┴
typ └┘ ┴ └──────┘ ┴ └───┘ ┴ └──────┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └┘ └──────┘ └───┘ └┘
124 let S : set ℝ := {y : ℝ | of y < x} in
id └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ └┘ ┴
typ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └┘
125 let R : _ := real.Sup S in
id ┴ └──────┘ ┴
src └──────┘
typ ┴ └──────┘ ┴
126 have hnile : _ := not_forall.mp (not_or_distrib.mp hni).1,
id └────────┘└─┘ └────────────┘└─┘ └─┘ ┴
src └────────┘└─┘ └────────────┘└─┘ ┴
typ └────────┘└─┘ └────────────┘└─┘ └─┘ ┴
127 have hnige : _ := not_forall.mp (not_or_distrib.mp hni).2,
id └────────┘└─┘ └────────────┘└─┘ └─┘ ┴
src └────────┘└─┘ └────────────┘└─┘ ┴
typ └────────┘└─┘ └────────────┘└─┘ └─┘ ┴
128 Exists.dcases_on hnile $ Exists.dcases_on hnige $ λ r₁ hr₁ r₂ hr₂,
id └──────────────┘ └───┘ └──────────────┘ └───┘ └┘ └─┘ └┘ └─┘
src └──────────────┘ └──────────────┘
typ └──────────────┘ └───┘ └──────────────┘ └───┘ └┘ └─┘ └┘ └─┘
129 have HR₁ : ∃ y : ℝ, y ∈ S :=
id ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴
130 ⟨ r₁ - 1, lt_of_lt_of_le (of_lt_of_lt U (sub_one_lt _)) (not_lt.mp hr₁) ⟩,
id └┘ ┴ └────────────┘ └─────────┘ ┴ └────────┘ └────┘└─┘ └─┘
src ┴ └────────────┘ └─────────┘ ┴ └────────┘ └────┘└─┘
typ └┘ ┴ └────────────┘ └─────────┘ ┴ └────────┘ └────┘└─┘ └─┘
131 have HR₂ : ∃ z : ℝ, ∀ y ∈ S, y ≤ z :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
132 ⟨ r₂, λ y hy, le_of_lt ((of_lt U).mpr (lt_of_lt_of_le hy (not_lt.mp hr₂))) ⟩,
id └┘ ┴ └┘ └──────┘ └───┘ ┴ └─┘ └────────────┘ └┘ └────┘└─┘ └─┘
src └──────┘ └───┘ ┴ └─┘ └────────────┘ └────┘└─┘
typ └┘ ┴ └┘ └──────┘ └───┘ ┴ └─┘ └────────────┘ └┘ └────┘└─┘ └─┘
133 λ δ hδ,
id ┴ └┘
typ ┴ └┘
134 ⟨ lt_of_not_ge' $ λ c,
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
135 have hc : ∀ y ∈ S, y ≤ R - δ := λ y hy, (of_le U.1).mpr $ le_of_lt $ lt_of_lt_of_le hy c,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───┘ ┴┴ └─┘ └──────┘ └────────────┘ └┘ ┴
src ┴ ┴ └───┘ ┴┴ └─┘ └──────┘ └────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───┘ ┴┴ └─┘ └──────┘ └────────────┘ └┘ ┴
136 not_lt_of_le ((real.Sup_le _ HR₁ HR₂).mpr hc) $ sub_lt_self R hδ,
id └──────────┘ └─────────┘ └─┘ └─┘ └─┘ └┘ └─────────┘ ┴ └┘
src └──────────┘ └─────────┘ └─┘ └─────────┘
typ └──────────┘ └─────────┘ └─┘ └─┘ └─┘ └┘ └─────────┘ ┴ └┘
137 lt_of_not_ge' $ λ c,
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
138 have hc : of (R + δ / 2) < x :=
id └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
139 lt_of_lt_of_le (add_lt_add_left (of_lt_of_lt U (half_lt_self hδ)) (of R)) c,
id └────────────┘ └─────────────┘ └─────────┘ ┴ └──────────┘ └┘ └┘ ┴ ┴
src └────────────┘ └─────────────┘ └─────────┘ ┴ └──────────┘ └┘
typ └────────────┘ └─────────────┘ └─────────┘ ┴ └──────────┘ └┘ └┘ ┴ ┴
doc └┘
140 not_lt_of_le (real.le_Sup _ HR₂ hc) $ (lt_add_iff_pos_right _).mpr $ half_pos hδ⟩
id └──────────┘ └─────────┘ └─┘ └┘ └──────────────────┘ └─┘ └──────┘ └┘
src └──────────┘ └─────────┘ └──────────────────┘ └─┘ └──────┘
typ └──────────┘ └─────────┘ └─┘ └┘ └──────────────────┘ └─┘ └──────┘ └┘
141
142 theorem exists_st_of_not_infinite {x : ℝ*} (hni : ¬ infinite x) : ∃ r : ℝ, is_st x r :=
id └┘ ┴ └──────┘ ┴ ┴ ┴┴ └───┘ ┴ ┴
src └┘ ┴ └──────┘ ┴ ┴┴ └───┘
typ └┘ ┴ └──────┘ ┴ ┴ ┴┴ └───┘ ┴ ┴
doc └┘ └──────┘ └───┘
143 ⟨ real.Sup {y : ℝ | of y < x}, is_st_Sup hni ⟩
id └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───────┘ └─┘
src └──────┘ ┴ ┴ └┘ ┴ └───────┘
typ └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───────┘ └─┘
doc └┘
144
145 theorem st_eq_Sup {x : ℝ*} : st x = real.Sup {y : ℝ | of y < x} :=
id └┘ └┘ ┴ ┴ └──────┘ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ └┘ ┴ └──────┘ ┴ ┴ └┘ ┴
typ └┘ └┘ ┴ ┴ └──────┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └┘ └┘ └┘
146 begin
st └─────
147 unfold st, split_ifs,
src └───────┘ └───────┘
typ └───────┘ └───────┘
doc └───────┘ └───────┘
txt └───────┘ └───────┘
par └───────┘ └───────┘
pid └─┘
st ────────┘└─────────┘└─
148 { exact is_st_unique (classical.some_spec h) (is_st_Sup (not_infinite_of_exists_st h)) },
id └──────────┘ └─────────────────┘ └───────┘ └───────────────────────┘ ┴
src └────┘└──────────┘┴ └─────────────────┘┴ └┘ └───────┘┴ └───────────────────────┘┴ └─┘
typ └────┘└──────────┘┴ └─────────────────┘┴ └┘ └───────┘┴ └───────────────────────┘┴┴└─┘
doc └────┘ ┴ ┴ └┘ ┴ ┴ └─┘
txt └────┘ ┴ ┴ └┘ ┴ ┴ └─┘
par └────┘ ┴ ┴ └┘ ┴ ┴ └─┘
pid ┴ ┴ ┴ └┘ ┴ ┴ └┘┴
st ─┘└───────────────────────────────────────────────────────────────────────────────────┘└┘└
149 { cases not_imp_comm.mp exists_st_of_not_infinite h with H H,
id └─────────────┘ └───────────────────────┘ ┴
src └────┘└─────────────┘┴└───────────────────────┘┴ └───────┘
typ └────┘└─────────────┘┴└───────────────────────┘┴┴└───────┘
doc └────┘ ┴ ┴ └───────┘
txt └────┘ ┴ ┴ └───────┘
par └────┘ ┴ ┴ └───────┘
pid ┴ ┴ ┴ └───────┘
st ───────────────────────────────────────────────────────────┘└─
150 { rw (set.ext (λ i, ⟨λ hi, set.mem_univ i, λ hi, H i⟩) : {y : ℝ | of y < x} = set.univ),
id └─────┘ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └──────┘
src └─┘ └─────┘┴ └──┘ └───┘└──────────┘┴ └┘ └───┘ ┴ └───┘┴└──┘ └─┘└┘┴ ┴┴┴ └┘┴┴└──────┘┴
typ └─┘ └─────┘┴ └──┘ └───┘└──────────┘┴ └┘ └───┘┴┴ └───┘┴└──┘ └─┘└┘┴ ┴┴┴┴└┘┴┴└──────┘┴
doc └─┘ ┴ └──┘ └───┘ ┴ └┘ └───┘ ┴ └───┘ └──┘ └─┘└┘┴ ┴ ┴ └┘ ┴ ┴
txt └─┘ ┴ └──┘ └───┘ ┴ └┘ └───┘ ┴ └───┘ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴
par └─┘ ┴ └──┘ └───┘ ┴ └┘ └───┘ ┴ └───┘ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴
pid ┴ ┴ └──┘ └───┘ ┴ └┘ └───┘ ┴ └───┘ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴
st ───┘└───────────────────────────────────────────────────────────────────────────────────┘└─
151 exact (real.Sup_univ).symm },
id └───────────┘
src └────┘ └───────────┘└─────┘
typ └────┘ └───────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └───┘└┘
st ──────────────────────────────┘└┘└
152 { rw (set.ext (λ i, ⟨λ hi, false.elim (not_lt_of_lt (H i) hi),
id └─────┘ └──────────┘ ┴
src └─┘ └─────┘┴ └──┘ └───┘ ┴ └──────────┘┴ ┴ └┘ └──
typ └─┘ └─────┘┴ └──┘ └───┘ ┴ └──────────┘┴ ┴┴ └┘ └──
doc └─┘ ┴ └──┘ └───┘ ┴ ┴ ┴ └┘ └──
txt └─┘ ┴ └──┘ └───┘ ┴ ┴ ┴ └┘ └──
par └─┘ ┴ └──┘ └───┘ ┴ ┴ ┴ └┘ └──
pid ┴ ┴ └──┘ └───┘ ┴ ┴ ┴ └┘ └──
st ─────────────────────────────────────────────────────────────────
153 λ hi, false.elim (set.not_mem_empty i hi)⟩) : {y : ℝ | of y < x} = ∅),
id └────────┘ └───────────────┘ ┴ └┘ ┴ ┴
src ───┘ └───┘└────────┘┴ └───────────────┘┴ ┴ └────┘┴└──┘ └─┘└┘┴ ┴ ┴ └┘ ┴┴┴
typ ───┘ └───┘└────────┘┴ └───────────────┘┴ ┴ └────┘┴└──┘ └─┘└┘┴ ┴ ┴┴└┘ ┴┴┴
doc ───┘ └───┘ ┴ ┴ ┴ └────┘ └──┘ └─┘└┘┴ ┴ ┴ └┘ ┴ ┴
txt ───┘ └───┘ ┴ ┴ ┴ └────┘ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴
par ───┘ └───┘ ┴ ┴ ┴ └────┘ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴
pid ───┘ └───┘ ┴ ┴ ┴ └────┘ └──┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────────┘└─
154 exact (real.Sup_empty).symm } }
id └────────────┘
src └────┘ └────────────┘└─────┘
typ └────┘ └────────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └───┘└┘
st ───────────────────────────────┘└───
155 end
st ──┘
156
157 theorem exists_st_iff_not_infinite {x : ℝ*} : (∃ r : ℝ, is_st x r) ↔ ¬ infinite x :=
id └┘ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └┘ ┴ ┴┴ └───┘ ┴ ┴ └──────┘
typ └┘ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └┘ └───┘ └──────┘
158 ⟨ not_infinite_of_exists_st, exists_st_of_not_infinite ⟩
id └───────────────────────┘ └───────────────────────┘
src └───────────────────────┘ └───────────────────────┘
typ └───────────────────────┘ └───────────────────────┘
159
160 theorem infinite_iff_not_exists_st {x : ℝ*} : infinite x ↔ ¬ ∃ r : ℝ, is_st x r :=
id └┘ └──────┘ ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴
src └┘ └──────┘ ┴ ┴ ┴ ┴┴ └───┘
typ └┘ └──────┘ ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴
doc └┘ └──────┘ └───┘
161 iff_not_comm.mp exists_st_iff_not_infinite
id └──────────┘└─┘ └────────────────────────┘
src └──────────┘└─┘ └────────────────────────┘
typ └──────────┘└─┘ └────────────────────────┘
162
163 theorem st_infinite {x : ℝ*} (hi : infinite x) : st x = 0 :=
id └┘ └──────┘ ┴ └┘ ┴ ┴
src └┘ └──────┘ └┘ ┴
typ └┘ └──────┘ ┴ └┘ ┴ ┴
doc └┘ └──────┘ └┘
164 begin
st └─────
165 unfold st, split_ifs,
src └───────┘ └───────┘
typ └───────┘ └───────┘
doc └───────┘ └───────┘
txt └───────┘ └───────┘
par └───────┘ └───────┘
pid └─┘
st ──────────┘└─────────┘└─
166 { exact false.elim ((infinite_iff_not_exists_st.mp hi) h) },
id └────────┘ └───────────────────────────┘ └┘ ┴
src └────┘└────────┘┴ └───────────────────────────┘┴ └┘ └┘
typ └────┘└────────┘┴ └───────────────────────────┘┴└┘└┘┴└┘
doc └────┘ ┴ ┴ └┘ └┘
txt └────┘ ┴ ┴ └┘ └┘
par └────┘ ┴ ┴ └┘ └┘
pid ┴ ┴ ┴ └┘ ┴┴
st ───┘└──────────────────────────────────────────────────────┘└┘└
167 { refl }
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────┘└─
168 end
st ──┘
169
170 lemma st_of_is_st {x : ℝ*} {r : ℝ} (hxr : is_st x r) : st x = r :=
id └┘ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴
src └┘ ┴ └───┘ └┘ ┴
typ └┘ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └┘ └───┘ └┘
171 begin
st └─────
172 unfold st, split_ifs,
src └───────┘ └───────┘
typ └───────┘ └───────┘
doc └───────┘ └───────┘
txt └───────┘ └───────┘
par └───────┘ └───────┘
pid └─┘
st ──────────┘└─────────┘└─
173 { exact is_st_unique (classical.some_spec h) hxr },
id └──────────┘ └─────────────────┘ ┴ └─┘
src └────┘└──────────┘┴ └─────────────────┘┴ └┘ ┴
typ └────┘└──────────┘┴ └─────────────────┘┴┴└┘└─┘┴
doc └────┘ ┴ ┴ └┘ ┴
txt └────┘ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ └┘ ┴
st ───┘└─────────────────────────────────────────────┘└┘└
174 { exact false.elim (h ⟨r, hxr⟩) }
id └────────┘ ┴ ┴ └─┘
src └────┘└────────┘┴ ┴ └┘ └─┘
typ └────┘└────────┘┴ ┴┴ ┴└┘└─┘└─┘
doc └────┘ ┴ ┴ └┘ └─┘
txt └────┘ ┴ ┴ └┘ └─┘
par └────┘ ┴ ┴ └┘ └─┘
pid ┴ ┴ ┴ └┘ └┘┴
st ─────────────────────────────────┘└─
175 end
st ──┘
176
177 lemma is_st_st_of_is_st {x : ℝ*} {r : ℝ} (hxr : is_st x r) : is_st x (st x) :=
id └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ └┘ ┴
src └┘ ┴ └───┘ └───┘ └┘
typ └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ └┘ ┴
doc └┘ └───┘ └───┘ └┘
178 by rwa [st_of_is_st hxr]
id └─────────┘ └─┘
src └───┘└─────────┘┴ └─
typ └───┘└─────────┘┴└─┘└─
doc └───┘ ┴ └─
txt └───┘ ┴ └─
par └───┘ ┴ └─
pid └┘ ┴ ┴└
st └───────────────────┘┴└
179
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
180 lemma is_st_st_of_exists_st {x : ℝ*} (hx : ∃ r : ℝ, is_st x r) : is_st x (st x) :=
id └┘ ┴ ┴┴ └───┘ ┴ ┴ └───┘ ┴ └┘ ┴
src └┘ ┴ ┴┴ └───┘ └───┘ └┘
typ └┘ ┴ ┴┴ └───┘ ┴ ┴ └───┘ ┴ └┘ ┴
doc └┘ └───┘ └───┘ └┘
181 Exists.dcases_on hx (λ r, is_st_st_of_is_st)
id └──────────────┘ └┘ ┴ └───────────────┘
src └──────────────┘ └───────────────┘
typ └──────────────┘ └┘ ┴ └───────────────┘
182
183 lemma is_st_st {x : ℝ*} (hx : st x ≠ 0) : is_st x (st x) :=
id └┘ └┘ ┴ ┴ └───┘ ┴ └┘ ┴
src └┘ └┘ ┴ └───┘ └┘
typ └┘ └┘ ┴ ┴ └───┘ ┴ └┘ ┴
doc └┘ └┘ └───┘ └┘
184 begin
st └─────
185 unfold st, split_ifs,
src └───────┘ └───────┘
typ └───────┘ └───────┘
doc └───────┘ └───────┘
txt └───────┘ └───────┘
par └───────┘ └───────┘
pid └─┘
st ──────────┘└─────────┘└─
186 { exact classical.some_spec h },
id └─────────────────┘ ┴
src └────┘└─────────────────┘┴ ┴
typ └────┘└─────────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───┘└──────────────────────────┘└┘└
187 { exact false.elim (hx (by unfold st; split_ifs; refl)) }
id └────────┘ └┘
src └────┘└────────┘┴ ┴ ┴└───────┘└┘└───────┘└┘└──┘└─┘
typ └────┘└────────┘┴ └┘┴ ┴└───────┘└┘└───────┘└┘└──┘└─┘
doc └────┘ ┴ ┴ ┴└───────┘└┘└───────┘└┘└──┘└─┘
txt └────┘ ┴ ┴ ┴└───────┘└┘└───────┘└┘└──┘└─┘
par └────┘ ┴ ┴ ┴└───────┘└┘└───────┘└┘└──┘└─┘
pid ┴ ┴ ┴ └───────────────────────────┘┴
st ───────────────────────────┘└─────────────────────────┘└─┘└─
188 end
st ──┘
189
190 lemma is_st_st' {x : ℝ*} (hx : ¬ infinite x) : is_st x (st x) :=
id └┘ ┴ └──────┘ ┴ └───┘ ┴ └┘ ┴
src └┘ ┴ └──────┘ └───┘ └┘
typ └┘ ┴ └──────┘ ┴ └───┘ ┴ └┘ ┴
doc └┘ └──────┘ └───┘ └┘
191 is_st_st_of_exists_st $ exists_st_of_not_infinite hx
id └───────────────────┘ └───────────────────────┘ └┘
src └───────────────────┘ └───────────────────────┘
typ └───────────────────┘ └───────────────────────┘ └┘
192
193 lemma is_st_refl_real (r : ℝ) : is_st r r :=
id ┴ └───┘ ┴ ┴
src ┴ └───┘
typ ┴ └───┘ ┴ ┴
doc └───┘
194 λ δ hδ, ⟨ sub_lt_self _ (of_lt_of_lt U hδ), (lt_add_of_pos_right _ (of_lt_of_lt U hδ)) ⟩
id ┴ └┘ └─────────┘ └─────────┘ ┴ └┘ └─────────────────┘ └─────────┘ ┴ └┘
src └─────────┘ └─────────┘ ┴ └─────────────────┘ └─────────┘ ┴
typ ┴ └┘ └─────────┘ └─────────┘ ┴ └┘ └─────────────────┘ └─────────┘ ┴ └┘
195
196 lemma st_id_real (r : ℝ) : st r = r := st_of_is_st (is_st_refl_real r)
id ┴ └┘ ┴ ┴ ┴ └─────────┘ └─────────────┘ ┴
src ┴ └┘ ┴ └─────────┘ └─────────────┘
typ ┴ └┘ ┴ ┴ ┴ └─────────┘ └─────────────┘ ┴
doc └┘
197
198 lemma eq_of_is_st_real {r s : ℝ} : is_st r s → r = s := is_st_unique (is_st_refl_real r)
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ └─────────────┘ ┴
src ┴ └───┘ ┴ └──────────┘ └─────────────┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ └─────────────┘ ┴
doc └───┘
199
200 lemma is_st_real_iff_eq {r s : ℝ} : is_st r s ↔ r = s :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
201 ⟨eq_of_is_st_real, λ hrs, by rw [hrs]; exact is_st_refl_real s⟩
id └──────────────┘ └─┘ └─┘ └─────────────┘ ┴
src └──────────────┘ └──┘ ┴ └────┘└─────────────┘┴
typ └──────────────┘ └─┘ └──┘└─┘┴ └────┘└─────────────┘┴┴
doc └──┘ ┴ └────┘ ┴
txt └──┘ ┴ └────┘ ┴
par └──┘ ┴ └────┘ ┴
pid └┘ ┴ ┴ ┴
st └──────┘┴└───────────────────────┘
202
203 lemma is_st_symm_real {r s : ℝ} : is_st r s ↔ is_st s r :=
id ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴
doc └───┘ └───┘
204 by rw [is_st_real_iff_eq, is_st_real_iff_eq, eq_comm]
id └───────────────┘ └───────────────┘ └─────┘
src └──┘└───────────────┘└┘└───────────────┘└┘└─────┘└─
typ └──┘└───────────────┘└┘└───────────────┘└┘└─────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └────────────────────┘└─────────────────┘└───────┘┴└
205
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
206 lemma is_st_trans_real {r s t : ℝ} : is_st r s → is_st s t → is_st r t :=
id ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴
src ┴ └───┘ └───┘ └───┘
typ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴
doc └───┘ └───┘ └───┘
207 by rw [is_st_real_iff_eq, is_st_real_iff_eq, is_st_real_iff_eq]; exact eq.trans
id └───────────────┘ └───────────────┘ └───────────────┘ └──────┘
src └──┘└───────────────┘└┘└───────────────┘└┘└───────────────┘┴ └────┘└──────┘└
typ └──┘└───────────────┘└┘└───────────────┘└┘└───────────────┘┴ └────┘└──────┘└
doc └──┘ └┘ └┘ ┴ └────┘ └
txt └──┘ └┘ └┘ ┴ └────┘ └
par └──┘ └┘ └┘ ┴ └────┘ └
pid └┘ └┘ └┘ ┴ ┴ └
st └────────────────────┘└─────────────────┘└─────────────────┘┴└────────────────
208
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
209 lemma is_st_inj_real {r₁ r₂ s : ℝ} (h1 : is_st r₁ s) (h2 : is_st r₂ s) : r₁ = r₂ :=
id ┴ └───┘ └┘ ┴ └───┘ └┘ ┴ └┘ ┴ └┘
src ┴ └───┘ └───┘ ┴
typ ┴ └───┘ └┘ ┴ └───┘ └┘ ┴ └┘ ┴ └┘
doc └───┘ └───┘
210 eq.trans (eq_of_is_st_real h1) (eq_of_is_st_real h2).symm
id └──────┘ └──────────────┘ └┘ └──────────────┘ └┘ └──┘
src └──────┘ └──────────────┘ └──────────────┘ └──┘
typ └──────┘ └──────────────┘ └┘ └──────────────┘ └┘ └──┘
211
212 lemma is_st_iff_abs_sub_lt_delta {x : ℝ*} {r : ℝ} :
id └┘ ┴
src └┘ ┴
typ └┘ ┴
doc └┘
213 is_st x r ↔ ∀ (δ : ℝ), δ > 0 → abs (x - r) < δ :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ └─┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
doc └───┘
214 by simp only [abs_sub_lt_iff, @sub_lt _ _ (r : ℝ*) x _,
id └────────────┘ └────┘ ┴ ┴
src └─────────┘└────────────┘└┘ └────┘└───┘ └─┘ └┘ └───
typ └─────────┘└────────────┘└┘ └────┘└───┘ ┴└─┘ └┘┴└───
doc └─────────┘ └┘ └───┘ └─┘ └┘ └───
txt └─────────┘ └┘ └───┘ └─┘ └┘ └───
par └─────────┘ └┘ └───┘ └─┘ └┘ └───
pid ┴└──┘└┘ └┘ └───┘ └─┘ └┘ └───
st └─────────────────────────────────────────────────────
215 @sub_lt_iff_lt_add' _ _ x (r : ℝ*) _, and_comm]; refl
id └────────────────┘ ┴ ┴ └──────┘
src ───┘ └────────────────┘└───┘ ┴ └─┘ └───┘└──────┘┴ └────
typ ───┘ └────────────────┘└───┘┴┴ ┴└─┘ └───┘└──────┘┴ └────
doc ───┘ └───┘ ┴ └─┘ └───┘ ┴ └────
txt ───┘ └───┘ ┴ └─┘ └───┘ ┴ └────
par ───┘ └───┘ ┴ └─┘ └───┘ ┴ └────
pid ───┘ └───┘ ┴ └─┘ └───┘ ┴ └
st ──────────────────────────────────────────────────────────
216
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
217 lemma is_st_add {x y : ℝ*} {r s : ℝ} : is_st x r → is_st y s → is_st (x + y) (r + s) :=
id └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └───┘ └───┘ └───┘ ┴ ┴
typ └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └───┘ └───┘ └───┘
218 λ hxr hys d hd,
id └─┘ └─┘ ┴ └┘
typ └─┘ └─┘ ┴ └┘
219 have hxr' : _ := hxr (d / 2) (half_pos hd), have hys' : _ := hys (d / 2) (half_pos hd),
id └─┘ ┴ ┴ └──────┘ └┘ └─┘ ┴ ┴ └──────┘ └┘
src ┴ └──────┘ ┴ └──────┘
typ └─┘ ┴ ┴ └──────┘ └┘ └─┘ ┴ ┴ └──────┘ └┘
220 by rw [←of_eq_coe, ←of_eq_coe, ←add_halves d, of_add, of_add, add_sub_comm,
id └───────┘ └───────┘ └────────┘ ┴ └────┘ └────┘ └──────────┘
src └───┘└───────┘└─┘└───────┘└─┘└────────┘┴ └┘└────┘└┘└────┘└┘└──────────┘└─
typ └───┘└───────┘└─┘└───────┘└─┘└────────┘┴┴└┘└────┘└┘└────┘└┘└──────────┘└─
doc └───┘ └─┘ └─┘ ┴ └┘ └┘ └┘ └─
txt └───┘ └─┘ └─┘ ┴ └┘ └┘ └┘ └─
par └───┘ └─┘ └─┘ ┴ └┘ └┘ └┘ └─
pid └─┘ └─┘ └─┘ ┴ └┘ └┘ └┘ └─
st └─────────────┘└──────────┘└─────────────┘└──────┘└──────┘└────────────┘└─
221 norm_num.add_comm_middle, ←add_assoc, add_assoc _ _ (of s), add_comm _ (of s)];
id └──────────────────────┘ └───────┘ └───────┘ └┘ ┴ └──────┘ └┘ ┴
src ──────┘└──────────────────────┘└─┘└───────┘└┘└───────┘└───┘ └┘┴ └─┘└──────┘└─┘ └┘┴ └┘
typ ──────┘└──────────────────────┘└─┘└───────┘└┘└───────┘└───┘ └┘┴┴└─┘└──────┘└─┘ └┘┴┴└┘
doc ──────┘ └─┘ └┘ └───┘ └┘┴ └─┘ └─┘ └┘┴ └┘
txt ──────┘ └─┘ └┘ └───┘ ┴ └─┘ └─┘ ┴ └┘
par ──────┘ └─┘ └┘ └───┘ ┴ └─┘ └─┘ ┴ └┘
pid ──────┘ └─┘ └┘ └───┘ ┴ └─┘ └─┘ ┴ └┘
st ──────────────────────────────┘└──────────┘└────────────────────┘└─────────────────┘┴└─
222 exact ⟨ add_lt_add hxr'.1 hys'.1, add_lt_add hxr'.2 hys'.2 ⟩
id └────────┘ └──┘ └──┘
src └────┘ ┴ ┴ └─┘ └──┘└────────┘┴ └─┘ └────
typ └────┘ ┴ ┴ └─┘ └──┘└────────┘┴└──┘└─┘└──┘└────
doc └────┘ ┴ ┴ └─┘ └──┘ ┴ └─┘ └────
txt └────┘ ┴ ┴ └─┘ └──┘ ┴ └─┘ └────
par └────┘ ┴ ┴ └─┘ └──┘ ┴ └─┘ └────
pid ┴ ┴ ┴ └─┘ └──┘ ┴ └─┘ └──┘└
st ─────────────────────────────────────────────────────────────
223
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
224 lemma is_st_neg {x : ℝ*} {r : ℝ} (hxr : is_st x r) : is_st (-x) (-r) :=
id └┘ ┴ └───┘ ┴ ┴ └───┘ ┴┴ ┴┴
src └┘ ┴ └───┘ └───┘ ┴ ┴
typ └┘ ┴ └───┘ ┴ ┴ └───┘ ┴┴ ┴┴
doc └┘ └───┘ └───┘
225 λ d hd, by show -(r : ℝ*) - d < -x ∧ -x < -r + d; cases (hxr d hd); split; linarith
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
src └───┘┴ └─┘ └┘┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ └────┘ ┴ ┴ ┴ └───┘ └────────
typ ┴ └┘ └───┘┴ └─┘ └┘┴┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴┴┴┴┴ └────┘ └─┘┴┴┴└┘┴ └───┘ └────────
doc └───┘ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └───┘ └────────
txt └───┘ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └───┘ └────────
par └───┘ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └───┘ └────────
pid └───┘ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └
st └─────────────────────────────────────────────────────────────────────────
226
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
227 lemma is_st_sub {x y : ℝ*} {r s : ℝ} : is_st x r → is_st y s → is_st (x - y) (r - s) :=
id └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └───┘ └───┘ └───┘ ┴ ┴
typ └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └───┘ └───┘ └───┘
228 λ hxr hys, by rw [sub_eq_add_neg, sub_eq_add_neg]; exact is_st_add hxr (is_st_neg hys)
id └─┘ └─┘ └────────────┘ └────────────┘ └───────┘ └─┘ └───────┘ └─┘
src └──┘└────────────┘└┘└────────────┘┴ └────┘└───────┘┴ ┴ └───────┘┴ └─
typ └─┘ └─┘ └──┘└────────────┘└┘└────────────┘┴ └────┘└───────┘┴└─┘┴ └───────┘┴└─┘└─
doc └──┘ └┘ ┴ └────┘ ┴ ┴ ┴ └─
txt └──┘ └┘ ┴ └────┘ ┴ ┴ ┴ └─
par └──┘ └┘ ┴ └────┘ ┴ ┴ ┴ └─
pid └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴└
st └─────────────────┘└──────────────┘┴└─────────────────────────────────────
229
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
230 /- (st x < st y) → (x < y) → (x ≤ y) → (st x ≤ st y) -/
src ────────────────────────────────────────────────────────
typ ────────────────────────────────────────────────────────
doc ────────────────────────────────────────────────────────
txt ────────────────────────────────────────────────────────
par ────────────────────────────────────────────────────────
pid ────────────────────────────────────────────────────────
st ────────────────────────────────────────────────────────
231
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
232 lemma lt_of_is_st_lt {x y : ℝ*} {r s : ℝ} (hxr : is_st x r) (hys : is_st y s) :
id └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴
src └┘ ┴ └───┘ └───┘
typ └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴
doc └┘ └───┘ └───┘
233 r < s → x < y :=
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
234 λ hrs, have hrs' : 0 < (s - r) / 2 := half_pos (sub_pos.mpr hrs),
id └─┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └─────┘└──┘ └─┘
src ┴ ┴ ┴ └──────┘ └─────┘└──┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └─────┘└──┘ └─┘
235 have hxr' : _ := (hxr _ hrs').2, have hys' : _ := (hys _ hrs').1,
id └─┘ └──┘ ┴ └─┘ └──┘ ┴
src ┴ ┴
typ └─┘ └──┘ ┴ └─┘ └──┘ ┴
236 have H1 : r + ((s - r) / 2) = (r + s) / 2 := by linarith,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st └───────┘
237 have H2 : s - ((s - r) / 2) = (r + s) / 2 := by linarith,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st └───────┘
238 by simp only [(of_eq_coe _).symm, (of_add _ _).symm, (of_sub _ _).symm, H1, H2] at hxr' hys';
id └───────┘ └────┘ └────┘ └┘ └┘
src └─────────┘ └───────┘└────────┘ └────┘└──────────┘ └────┘└──────────┘ └┘ └────────────┘
typ └─────────┘ └───────┘└────────┘ └────┘└──────────┘ └────┘└──────────┘└┘└┘└┘└────────────┘
doc └─────────┘ └────────┘ └──────────┘ └──────────┘ └┘ └────────────┘
txt └─────────┘ └────────┘ └──────────┘ └──────────┘ └┘ └────────────┘
par └─────────┘ └────────┘ └──────────┘ └──────────┘ └┘ └────────────┘
pid ┴└──┘└┘ └────────┘ └──────────┘ └──────────┘ └┘ ┴┴└──────────┘
st └───────────────────────────────────────────────────────────────────────────────────────────
239 exact lt_trans hxr' hys'
id └──────┘ └──┘ └──┘
src └────┘└──────┘┴ ┴ └
typ └────┘└──────┘┴└──┘┴└──┘└
doc └────┘ ┴ ┴ └
txt └────┘ ┴ ┴ └
par └────┘ ┴ ┴ └
pid ┴ ┴ ┴ └
st ─────────────────────────
240
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
241 lemma is_st_le_of_le {x y : ℝ*} {r s : ℝ} (hrx : is_st x r) (hsy : is_st y s) :
id └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴
src └┘ ┴ └───┘ └───┘
typ └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴
doc └┘ └───┘ └───┘
242 x ≤ y → r ≤ s := by rw [←not_lt, ←not_lt, not_imp_not]; exact lt_of_is_st_lt hsy hrx
id ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └────┘ └─────────┘ └────────────┘ └─┘ └─┘
src ┴ ┴ └───┘└────┘└─┘└────┘└┘└─────────┘┴ └────┘└────────────┘┴ ┴ └
typ ┴ ┴ ┴ ┴ ┴ ┴ └───┘└────┘└─┘└────┘└┘└─────────┘┴ └────┘└────────────┘┴└─┘┴└─┘└
doc └───┘ └─┘ └┘ ┴ └────┘ ┴ ┴ └
txt └───┘ └─┘ └┘ ┴ └────┘ ┴ ┴ └
par └───┘ └─┘ └┘ ┴ └────┘ ┴ ┴ └
pid └─┘ └─┘ └┘ ┴ ┴ ┴ ┴ └
st └──────────┘└───────┘└───────────┘┴└──────────────────────────────
243
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
244 lemma st_le_of_le {x y : ℝ*} (hix : ¬ infinite x) (hiy : ¬ infinite y) :
id └┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └┘ ┴ └──────┘ ┴ └──────┘
typ └┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴
doc └┘ └──────┘ └──────┘
245 x ≤ y → st x ≤ st y :=
id ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ └┘ ┴ └┘
typ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘
246 have hx' : _ := is_st_st' hix, have hy' : _ := is_st_st' hiy,
id └───────┘ └─┘ └───────┘ └─┘
src └───────┘ └───────┘
typ └───────┘ └─┘ └───────┘ └─┘
247 is_st_le_of_le hx' hy'
id └────────────┘ └─┘ └─┘
src └────────────┘
typ └────────────┘ └─┘ └─┘
248
249 lemma lt_of_st_lt {x y : ℝ*} (hix : ¬ infinite x) (hiy : ¬ infinite y) :
id └┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └┘ ┴ └──────┘ ┴ └──────┘
typ └┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴
doc └┘ └──────┘ └──────┘
250 st x < st y → x < y :=
id └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └┘ ┴ └┘ ┴
typ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └┘ └┘
251 have hx' : _ := is_st_st' hix, have hy' : _ := is_st_st' hiy,
id └───────┘ └─┘ └───────┘ └─┘
src └───────┘ └───────┘
typ └───────┘ └─┘ └───────┘ └─┘
252 lt_of_is_st_lt hx' hy'
id └────────────┘ └─┘ └─┘
src └────────────┘
typ └────────────┘ └─┘ └─┘
253
254 -- BASIC LEMMAS ABOUT INFINITE
255
256 lemma infinite_pos_def {x : ℝ*} : infinite_pos x ↔ ∀ r : ℝ, x > r := by rw iff_eq_eq; refl
id └┘ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
src └┘ └──────────┘ ┴ ┴ ┴ └─┘└───────┘ └────
typ └┘ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└───────┘ └────
doc └┘ └──────────┘ └─┘ └────
txt └─┘ └────
par └─┘ └────
pid ┴ └
st └───────────────────
257
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
258 lemma infinite_neg_def {x : ℝ*} : infinite_neg x ↔ ∀ r : ℝ, x < r := by rw iff_eq_eq; refl
id └┘ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
src └┘ └──────────┘ ┴ ┴ ┴ └─┘└───────┘ └────
typ └┘ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└───────┘ └────
doc └┘ └──────────┘ └─┘ └────
txt └─┘ └────
par └─┘ └────
pid ┴ └
st └───────────────────
259
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
260 lemma ne_zero_of_infinite {x : ℝ*} : infinite x → x ≠ 0 :=
id └┘ └──────┘ ┴ ┴ ┴
src └┘ └──────┘ ┴
typ └┘ └──────┘ ┴ ┴ ┴
doc └┘ └──────┘
261 λ hI h0, or.cases_on hI
id └┘ └┘ └─────────┘ └┘
src └─────────┘
typ └┘ └┘ └─────────┘ └┘
262 (λ hip, lt_irrefl (0 : ℝ*) ((by rwa ←h0 : infinite_pos 0) 0))
id └─┘ └───────┘ └┘ └┘ └──────────┘
src └───────┘ └┘ └───┘ ┴ └──────────┘
typ └─┘ └───────┘ └┘ └───┘└┘┴ └──────────┘
doc └┘ └───┘ ┴ └──────────┘
txt └───┘ ┴
par └───┘ ┴
pid └┘ ┴
st └───────┘
263 (λ hin, lt_irrefl (0 : ℝ*) ((by rwa ←h0 : infinite_neg 0) 0))
id └─┘ └───────┘ └┘ └┘ └──────────┘
src └───────┘ └┘ └───┘ ┴ └──────────┘
typ └─┘ └───────┘ └┘ └───┘└┘┴ └──────────┘
doc └┘ └───┘ ┴ └──────────┘
txt └───┘ ┴
par └───┘ ┴
pid └┘ ┴
st └───────┘
264
265 lemma not_infinite_zero : ¬ infinite 0 := λ hI, ne_zero_of_infinite hI rfl
id ┴ └──────┘ └┘ └─────────────────┘ └┘ └─┘
src ┴ └──────┘ └─────────────────┘ └─┘
typ ┴ └──────┘ └┘ └─────────────────┘ └┘ └─┘
doc └──────┘
266
267 lemma pos_of_infinite_pos {x : ℝ*} : infinite_pos x → x > 0 := λ hip, hip 0
id └┘ └──────────┘ ┴ ┴ ┴ └─┘ └─┘
src └┘ └──────────┘ ┴
typ └┘ └──────────┘ ┴ ┴ ┴ └─┘ └─┘
doc └┘ └──────────┘
268
269 lemma neg_of_infinite_neg {x : ℝ*} : infinite_neg x → x < 0 := λ hin, hin 0
id └┘ └──────────┘ ┴ ┴ ┴ └─┘ └─┘
src └┘ └──────────┘ ┴
typ └┘ └──────────┘ ┴ ┴ ┴ └─┘ └─┘
doc └┘ └──────────┘
270
271 lemma not_infinite_pos_of_infinite_neg {x : ℝ*} : infinite_neg x → ¬ infinite_pos x :=
id └┘ └──────────┘ ┴ ┴ └──────────┘ ┴
src └┘ └──────────┘ ┴ └──────────┘
typ └┘ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └┘ └──────────┘ └──────────┘
272 λ hn hp, not_lt_of_lt (hn 1) (hp 1)
id └┘ └┘ └──────────┘ └┘ └┘
src └──────────┘
typ └┘ └┘ └──────────┘ └┘ └┘
273
274 lemma not_infinite_neg_of_infinite_pos {x : ℝ*} : infinite_pos x → ¬ infinite_neg x :=
id └┘ └──────────┘ ┴ ┴ └──────────┘ ┴
src └┘ └──────────┘ ┴ └──────────┘
typ └┘ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └┘ └──────────┘ └──────────┘
275 imp_not_comm.mp not_infinite_pos_of_infinite_neg
id └──────────┘└─┘ └──────────────────────────────┘
src └──────────┘└─┘ └──────────────────────────────┘
typ └──────────┘└─┘ └──────────────────────────────┘
276
277 lemma infinite_neg_neg_of_infinite_pos {x : ℝ*} : infinite_pos x → infinite_neg (-x) :=
id └┘ └──────────┘ ┴ └──────────┘ ┴┴
src └┘ └──────────┘ └──────────┘ ┴
typ └┘ └──────────┘ ┴ └──────────┘ ┴┴
doc └┘ └──────────┘ └──────────┘
278 λ hp r, neg_lt.mp (hp (-r))
id └┘ ┴ └────┘└─┘ └┘ ┴┴
src └────┘└─┘ ┴
typ └┘ ┴ └────┘└─┘ └┘ ┴┴
279
280 lemma infinite_pos_neg_of_infinite_neg {x : ℝ*} : infinite_neg x → infinite_pos (-x) :=
id └┘ └──────────┘ ┴ └──────────┘ ┴┴
src └┘ └──────────┘ └──────────┘ ┴
typ └┘ └──────────┘ ┴ └──────────┘ ┴┴
doc └┘ └──────────┘ └──────────┘
281 λ hp r, lt_neg.mp (hp (-r))
id └┘ ┴ └────┘└─┘ └┘ ┴┴
src └────┘└─┘ ┴
typ └┘ ┴ └────┘└─┘ └┘ ┴┴
282
283 lemma infinite_pos_iff_infinite_neg_neg {x : ℝ*} : infinite_pos x ↔ infinite_neg (-x) :=
id └┘ └──────────┘ ┴ ┴ └──────────┘ ┴┴
src └┘ └──────────┘ ┴ └──────────┘ ┴
typ └┘ └──────────┘ ┴ ┴ └──────────┘ ┴┴
doc └┘ └──────────┘ └──────────┘
284 ⟨ infinite_neg_neg_of_infinite_pos, λ hin, neg_neg x ▸ infinite_pos_neg_of_infinite_neg hin ⟩
id └──────────────────────────────┘ └─┘ └─────┘ ┴ ┴ └──────────────────────────────┘ └─┘
src └──────────────────────────────┘ └─────┘ ┴ └──────────────────────────────┘
typ └──────────────────────────────┘ └─┘ └─────┘ ┴ ┴ └──────────────────────────────┘ └─┘
285
286 lemma infinite_neg_iff_infinite_pos_neg {x : ℝ*} : infinite_neg x ↔ infinite_pos (-x) :=
id └┘ └──────────┘ ┴ ┴ └──────────┘ ┴┴
src └┘ └──────────┘ ┴ └──────────┘ ┴
typ └┘ └──────────┘ ┴ ┴ └──────────┘ ┴┴
doc └┘ └──────────┘ └──────────┘
287 ⟨ infinite_pos_neg_of_infinite_neg, λ hin, neg_neg x ▸ infinite_neg_neg_of_infinite_pos hin ⟩
id └──────────────────────────────┘ └─┘ └─────┘ ┴ ┴ └──────────────────────────────┘ └─┘
src └──────────────────────────────┘ └─────┘ ┴ └──────────────────────────────┘
typ └──────────────────────────────┘ └─┘ └─────┘ ┴ ┴ └──────────────────────────────┘ └─┘
288
289 lemma infinite_iff_infinite_neg {x : ℝ*} : infinite x ↔ infinite (-x) :=
id └┘ └──────┘ ┴ ┴ └──────┘ ┴┴
src └┘ └──────┘ ┴ └──────┘ ┴
typ └┘ └──────┘ ┴ ┴ └──────┘ ┴┴
doc └┘ └──────┘ └──────┘
290 ⟨ λ hi, or.cases_on hi
id └┘ └─────────┘ └┘
src └─────────┘
typ └┘ └─────────┘ └┘
291 (λ hip, or.inr (infinite_neg_neg_of_infinite_pos hip))
id └─┘ └────┘ └──────────────────────────────┘ └─┘
src └────┘ └──────────────────────────────┘
typ └─┘ └────┘ └──────────────────────────────┘ └─┘
292 (λ hin, or.inl (infinite_pos_neg_of_infinite_neg hin)),
id └─┘ └────┘ └──────────────────────────────┘ └─┘
src └────┘ └──────────────────────────────┘
typ └─┘ └────┘ └──────────────────────────────┘ └─┘
293 λ hi, or.cases_on hi
id └┘ └─────────┘ └┘
src └─────────┘
typ └┘ └─────────┘ └┘
294 (λ hipn, or.inr (infinite_neg_iff_infinite_pos_neg.mpr hipn))
id └──┘ └────┘ └───────────────────────────────┘└──┘ └──┘
src └────┘ └───────────────────────────────┘└──┘
typ └──┘ └────┘ └───────────────────────────────┘└──┘ └──┘
295 (λ hinp, or.inl (infinite_pos_iff_infinite_neg_neg.mpr hinp))⟩
id └──┘ └────┘ └───────────────────────────────┘└──┘ └──┘
src └────┘ └───────────────────────────────┘└──┘
typ └──┘ └────┘ └───────────────────────────────┘└──┘ └──┘
296
297 lemma not_infinite_of_infinitesimal {x : ℝ*} : infinitesimal x → ¬ infinite x :=
id └┘ └───────────┘ ┴ ┴ └──────┘ ┴
src └┘ └───────────┘ ┴ └──────┘
typ └┘ └───────────┘ ┴ ┴ └──────┘ ┴
doc └┘ └───────────┘ └──────┘
298 λ hi hI, have hi' : _ := (hi 2 two_pos), or.dcases_on hI
id └┘ └┘ └┘ └─────┘ └──────────┘ └┘
src └─────┘ └──────────┘
typ └┘ └┘ └┘ └─────┘ └──────────┘ └┘
299 (λ hip, have hip' : _ := hip 2, not_lt_of_lt hip' (by convert hi'.2; exact (zero_add 2).symm))
id └─┘ └─┘ └──────────┘ └──┘ └─┘ └──────┘
src └──────────┘ └──────┘ └┘ └────┘ └──────┘└──────┘
typ └─┘ └─┘ └──────────┘ └──┘ └──────┘└─┘└┘ └────┘ └──────┘└──────┘
doc └──────┘ └┘ └────┘ └──────┘
txt └──────┘ └┘ └────┘ └──────┘
par └──────┘ └┘ └────┘ └──────┘
pid ┴ └┘ ┴ └─────┘┴
st └─────────────────────────────────────┘
300 (λ hin, have hin' : _ := hin (-2), not_lt_of_lt hin' (by convert hi'.1; exact (zero_sub 2).symm))
id └─┘ └─┘ ┴ └──────────┘ └──┘ └─┘ └──────┘
src ┴ └──────────┘ └──────┘ └┘ └────┘ └──────┘└──────┘
typ └─┘ └─┘ ┴ └──────────┘ └──┘ └──────┘└─┘└┘ └────┘ └──────┘└──────┘
doc └──────┘ └┘ └────┘ └──────┘
txt └──────┘ └┘ └────┘ └──────┘
par └──────┘ └┘ └────┘ └──────┘
pid ┴ └┘ ┴ └─────┘┴
st └─────────────────────────────────────┘
301
302 lemma not_infinitesimal_of_infinite {x : ℝ*} : infinite x → ¬ infinitesimal x :=
id └┘ └──────┘ ┴ ┴ └───────────┘ ┴
src └┘ └──────┘ ┴ └───────────┘
typ └┘ └──────┘ ┴ ┴ └───────────┘ ┴
doc └┘ └──────┘ └───────────┘
303 imp_not_comm.mp not_infinite_of_infinitesimal
id └──────────┘└─┘ └───────────────────────────┘
src └──────────┘└─┘ └───────────────────────────┘
typ └──────────┘└─┘ └───────────────────────────┘
304
305 lemma not_infinitesimal_of_infinite_pos {x : ℝ*} : infinite_pos x → ¬ infinitesimal x :=
id └┘ └──────────┘ ┴ ┴ └───────────┘ ┴
src └┘ └──────────┘ ┴ └───────────┘
typ └┘ └──────────┘ ┴ ┴ └───────────┘ ┴
doc └┘ └──────────┘ └───────────┘
306 λ hp, not_infinitesimal_of_infinite (or.inl hp)
id └┘ └───────────────────────────┘ └────┘ └┘
src └───────────────────────────┘ └────┘
typ └┘ └───────────────────────────┘ └────┘ └┘
307
308 lemma not_infinitesimal_of_infinite_neg {x : ℝ*} : infinite_neg x → ¬ infinitesimal x :=
id └┘ └──────────┘ ┴ ┴ └───────────┘ ┴
src └┘ └──────────┘ ┴ └───────────┘
typ └┘ └──────────┘ ┴ ┴ └───────────┘ ┴
doc └┘ └──────────┘ └───────────┘
309 λ hn, not_infinitesimal_of_infinite (or.inr hn)
id └┘ └───────────────────────────┘ └────┘ └┘
src └───────────────────────────┘ └────┘
typ └┘ └───────────────────────────┘ └────┘ └┘
310
311 lemma infinite_pos_iff_infinite_and_pos {x : ℝ*} : infinite_pos x ↔ (infinite x ∧ x > 0) :=
id └┘ └──────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └┘ └──────────┘ ┴ └──────┘ ┴ ┴
typ └┘ └──────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └┘ └──────────┘ └──────┘
312 ⟨ λ hip, ⟨or.inl hip, hip 0⟩,
id └─┘ └────┘ └─┘ └─┘
src └────┘
typ └─┘ └────┘ └─┘ └─┘
313 λ ⟨hi, hp⟩, hi.cases_on (λ hip, hip) (λ hin, false.elim (not_lt_of_lt hp (hin 0))) ⟩
id ┴└┘ └┘ └───────┘ └─┘ └─┘ └─┘ └────────┘ └──────────┘ └─┘
src └───────┘ └────────┘ └──────────┘
typ ┴└┘ └┘ └───────┘ └─┘ └─┘ └─┘ └────────┘ └──────────┘ └─┘
314
315 lemma infinite_neg_iff_infinite_and_neg {x : ℝ*} : infinite_neg x ↔ (infinite x ∧ x < 0) :=
id └┘ └──────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └┘ └──────────┘ ┴ └──────┘ ┴ ┴
typ └┘ └──────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └┘ └──────────┘ └──────┘
316 ⟨ λ hip, ⟨or.inr hip, hip 0⟩,
id └─┘ └────┘ └─┘ └─┘
src └────┘
typ └─┘ └────┘ └─┘ └─┘
317 λ ⟨hi, hp⟩, hi.cases_on (λ hin, false.elim (not_lt_of_lt hp (hin 0))) (λ hip, hip) ⟩
id ┴└┘ └┘ └───────┘ └─┘ └────────┘ └──────────┘ └─┘ └─┘ └─┘
src └───────┘ └────────┘ └──────────┘
typ ┴└┘ └┘ └───────┘ └─┘ └────────┘ └──────────┘ └─┘ └─┘ └─┘
318
319 lemma infinite_pos_iff_infinite_of_pos {x : ℝ*} (hp : x > 0) : infinite_pos x ↔ infinite x :=
id └┘ ┴ ┴ └──────────┘ ┴ ┴ └──────┘ ┴
src └┘ ┴ └──────────┘ ┴ └──────┘
typ └┘ ┴ ┴ └──────────┘ ┴ ┴ └──────┘ ┴
doc └┘ └──────────┘ └──────┘
320 by rw [infinite_pos_iff_infinite_and_pos]; exact ⟨λ hI, hI.1, λ hI, ⟨hI, hp⟩⟩
id └───────────────────────────────┘ └┘
src └──┘└───────────────────────────────┘┴ └────┘ └───┘ └──┘ └───┘ └┘ └──
typ └──┘└───────────────────────────────┘┴ └────┘ └───┘ └──┘ └───┘ └┘└┘└──
doc └──┘ ┴ └────┘ └───┘ └──┘ └───┘ └┘ └──
txt └──┘ ┴ └────┘ └───┘ └──┘ └───┘ └┘ └──
par └──┘ ┴ └────┘ └───┘ └──┘ └───┘ └┘ └──
pid └┘ ┴ ┴ └───┘ └──┘ └───┘ └┘ └┘└
st └────────────────────────────────────┘┴└────────────────────────────────────
321
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
322 lemma infinite_pos_iff_infinite_of_nonneg {x : ℝ*} (hp : x ≥ 0) : infinite_pos x ↔ infinite x :=
id └┘ ┴ ┴ └──────────┘ ┴ ┴ └──────┘ ┴
src └┘ ┴ └──────────┘ ┴ └──────┘
typ └┘ ┴ ┴ └──────────┘ ┴ ┴ └──────┘ ┴
doc └┘ └──────────┘ └──────┘
323 or.cases_on (lt_or_eq_of_le hp) (infinite_pos_iff_infinite_of_pos)
id └─────────┘ └────────────┘ └┘ └──────────────────────────────┘
src └─────────┘ └────────────┘ └──────────────────────────────┘
typ └─────────┘ └────────────┘ └┘ └──────────────────────────────┘
324 (λ h, by rw h.symm; exact
id ┴
src └─┘ └─────
typ ┴ └─┘└────┘ └─────
doc └─┘ └─────
txt └─┘ └─────
par └─┘ └─────
pid ┴ └
st └─────────────────
325 ⟨λ hIP, false.elim (not_infinite_zero (or.inl hIP)), λ hI, false.elim (not_infinite_zero hI)⟩)
id └────┘ └────────┘ └───────────────┘
src ─┘ └────┘ ┴ ┴ └────┘┴ └──┘ └───┘└────────┘┴ └───────────────┘┴ └┘
typ ─┘ └────┘ ┴ ┴ └────┘┴ └──┘ └───┘└────────┘┴ └───────────────┘┴ └┘
doc ─┘ └────┘ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ └┘
txt ─┘ └────┘ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ └┘
par ─┘ └────┘ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ └┘
pid ─┘ └────┘ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────────┘
326
327 lemma infinite_neg_iff_infinite_of_neg {x : ℝ*} (hn : x < 0) : infinite_neg x ↔ infinite x :=
id └┘ ┴ ┴ └──────────┘ ┴ ┴ └──────┘ ┴
src └┘ ┴ └──────────┘ ┴ └──────┘
typ └┘ ┴ ┴ └──────────┘ ┴ ┴ └──────┘ ┴
doc └┘ └──────────┘ └──────┘
328 by rw [infinite_neg_iff_infinite_and_neg]; exact ⟨λ hI, hI.1, λ hI, ⟨hI, hn⟩⟩
id └───────────────────────────────┘ └┘
src └──┘└───────────────────────────────┘┴ └────┘ └───┘ └──┘ └───┘ └┘ └──
typ └──┘└───────────────────────────────┘┴ └────┘ └───┘ └──┘ └───┘ └┘└┘└──
doc └──┘ ┴ └────┘ └───┘ └──┘ └───┘ └┘ └──
txt └──┘ ┴ └────┘ └───┘ └──┘ └───┘ └┘ └──
par └──┘ ┴ └────┘ └───┘ └──┘ └───┘ └┘ └──
pid └┘ ┴ ┴ └───┘ └──┘ └───┘ └┘ └┘└
st └────────────────────────────────────┘┴└────────────────────────────────────
329
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
330 lemma infinite_pos_abs_iff_infinite_abs {x : ℝ*} : infinite_pos (abs x) ↔ infinite (abs x) :=
id └┘ └──────────┘ └─┘ ┴ ┴ └──────┘ └─┘ ┴
src └┘ └──────────┘ └─┘ ┴ └──────┘ └─┘
typ └┘ └──────────┘ └─┘ ┴ ┴ └──────┘ └─┘ ┴
doc └┘ └──────────┘ └──────┘
331 infinite_pos_iff_infinite_of_nonneg (abs_nonneg _)
id └─────────────────────────────────┘ └────────┘
src └─────────────────────────────────┘ └────────┘
typ └─────────────────────────────────┘ └────────┘
332
333 lemma infinite_iff_infinite_pos_abs {x : ℝ*} : infinite x ↔ infinite_pos (abs x) :=
id └┘ └──────┘ ┴ ┴ └──────────┘ └─┘ ┴
src └┘ └──────┘ ┴ └──────────┘ └─┘
typ └┘ └──────┘ ┴ ┴ └──────────┘ └─┘ ┴
doc └┘ └──────┘ └──────────┘
334 ⟨ λ hi d, or.cases_on hi
id └┘ ┴ └─────────┘ └┘
src └─────────┘
typ └┘ ┴ └─────────┘ └┘
335 (λ hip, by rw [abs_of_pos (hip 0)]; exact hip d)
id └─┘ └────────┘ └─┘ └─┘ ┴
src └──┘└────────┘┴ └──┘ └────┘ ┴
typ └─┘ └──┘└────────┘┴ └─┘└──┘ └────┘└─┘┴┴
doc └──┘ ┴ └──┘ └────┘ ┴
txt └──┘ ┴ └──┘ └────┘ ┴
par └──┘ ┴ └──┘ └────┘ ┴
pid └┘ ┴ └──┘ ┴ ┴
st └─────────────────────┘┴└───────────┘
336 (λ hin, by rw [abs_of_neg (hin 0)]; exact lt_neg.mp (hin (-d))),
id └─┘ └────────┘ └─┘ └───────┘ └─┘ ┴┴
src └──┘└────────┘┴ └──┘ └────┘└───────┘┴ ┴ ┴ └┘
typ └─┘ └──┘└────────┘┴ └─┘└──┘ └────┘└───────┘┴ └─┘┴ ┴┴└┘
doc └──┘ ┴ └──┘ └────┘ ┴ ┴ └┘
txt └──┘ ┴ └──┘ └────┘ ┴ ┴ └┘
par └──┘ ┴ └──┘ └────┘ ┴ ┴ └┘
pid └┘ ┴ └──┘ ┴ ┴ ┴ └┘
st └─────────────────────┘┴└──────────────────────────┘
337 λ hipa, by { rcases (lt_trichotomy x 0) with h | h | h,
id └──┘ └───────────┘ ┴
src └─────┘ └───────────┘┴ └────────────────┘
typ └──┘ └─────┘ └───────────┘┴┴└────────────────┘
doc └─────┘ ┴ └────────────────┘
txt └─────┘ ┴ └────────────────┘
par └─────┘ ┴ └────────────────┘
pid ┴ ┴ └────────────────┘
st └──────────────────────────────────────────┘└─
338 { exact or.inr (infinite_neg_iff_infinite_pos_neg.mpr (by rwa abs_of_neg h at hipa)) },
id └────┘ └───────────────────────────────────┘ └────────┘ ┴
src └────┘└────┘┴ └───────────────────────────────────┘┴ ┴└──┘└────────┘┴ └──────┘└─┘
typ └────┘└────┘┴ └───────────────────────────────────┘┴ ┴└──┘└────────┘┴┴└──────┘└─┘
doc └────┘ ┴ ┴ ┴└──┘ ┴ └──────┘└─┘
txt └────┘ ┴ ┴ ┴└──┘ ┴ └──────┘└─┘
par └────┘ ┴ ┴ ┴└──┘ ┴ └──────┘└─┘
pid ┴ ┴ ┴ └───┘ ┴ └────────┘┴
st ─────┘└─────────────────────────────────────────────────────┘└───────────────────────┘└─┘└┘└
339 { exact false.elim (ne_zero_of_infinite (or.inl (by rw [h]; rwa [h, abs_zero] at hipa)) h) },
id └────────┘ └─────────────────┘ └────┘ ┴ ┴ └──────┘ ┴
src └────┘└────────┘┴ └─────────────────┘┴ └────┘┴ ┴└──┘ ┴└┘└───┘ └┘└──────┘└───────┘└─┘ └┘
typ └────┘└────────┘┴ └─────────────────┘┴ └────┘┴ ┴└──┘┴┴└┘└───┘┴└┘└──────┘└───────┘└─┘┴└┘
doc └────┘ ┴ ┴ ┴ ┴└──┘ ┴└┘└───┘ └┘ └───────┘└─┘ └┘
txt └────┘ ┴ ┴ ┴ ┴└──┘ ┴└┘└───┘ └┘ └───────┘└─┘ └┘
par └────┘ ┴ ┴ ┴ ┴└──┘ ┴└┘└───┘ └┘ └───────┘└─┘ └┘
pid ┴ ┴ ┴ ┴ └───┘ └──────┘ └┘ └──────────┘ ┴┴
st ─────┘└───────────────────────────────────────────────┘└────┘┴└─────┘┴└────────┘┴└──────┘└────┘└┘└
340 { exact or.inl (by rwa abs_of_pos h at hipa) } } ⟩
id └────┘ └────────┘ ┴
src └────┘└────┘┴ ┴└──┘└────────┘┴ └──────┘└┘
typ └────┘└────┘┴ ┴└──┘└────────┘┴┴└──────┘└┘
doc └────┘ ┴ ┴└──┘ ┴ └──────┘└┘
txt └────┘ ┴ ┴└──┘ ┴ └──────┘└┘
par └────┘ ┴ ┴└──┘ ┴ └──────┘└┘
pid ┴ ┴ └───┘ ┴ └───────┘┴
st ─────────────────────┘└───────────────────────┘└┘└──┘
341
342 lemma infinite_iff_infinite_abs {x : ℝ*} : infinite x ↔ infinite (abs x) :=
id └┘ └──────┘ ┴ ┴ └──────┘ └─┘ ┴
src └┘ └──────┘ ┴ └──────┘ └─┘
typ └┘ └──────┘ ┴ ┴ └──────┘ └─┘ ┴
doc └┘ └──────┘ └──────┘
343 by rw [←infinite_pos_iff_infinite_of_nonneg (abs_nonneg _), infinite_iff_infinite_pos_abs]
id └─────────────────────────────────┘ └────────┘ └───────────────────────────┘
src └───┘└─────────────────────────────────┘┴ └────────┘└───┘└───────────────────────────┘└─
typ └───┘└─────────────────────────────────┘┴ └────────┘└───┘└───────────────────────────┘└─
doc └───┘ ┴ └───┘ └─
txt └───┘ ┴ └───┘ └─
par └───┘ ┴ └───┘ └─
pid └─┘ ┴ └───┘ ┴└
st └──────────────────────────────────────────────────────┘└─────────────────────────────┘┴└
344
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
345 lemma infinite_iff_abs_lt_abs {x : ℝ*} : infinite x ↔ ∀ r : ℝ, (abs r : ℝ*) < abs x :=
id └┘ └──────┘ ┴ ┴ ┴ └─┘ ┴ └┘ ┴ └─┘ ┴
src └┘ └──────┘ ┴ ┴ └─┘ └┘ ┴ └─┘
typ └┘ └──────┘ ┴ ┴ ┴ └─┘ ┴ └┘ ┴ └─┘ ┴
doc └┘ └──────┘ └┘
346 ⟨ λ hI r, (of_abs U r) ▸ infinite_iff_infinite_pos_abs.mp hI (abs r),
id └┘ ┴ └────┘ ┴ ┴ ┴ └───────────────────────────┘└─┘ └┘ └─┘ ┴
src └────┘ ┴ ┴ └───────────────────────────┘└─┘ └─┘
typ └┘ ┴ └────┘ ┴ ┴ ┴ └───────────────────────────┘└─┘ └┘ └─┘ ┴
347 λ hR, or.cases_on (max_choice x (-x))
id └┘ └─────────┘ └────────┘ ┴ ┴┴
src └─────────┘ └────────┘ ┴
typ └┘ └─────────┘ └────────┘ ┴ ┴┴
348 (λ h, or.inl $ λ r, lt_of_le_of_lt (le_abs_self _) (h ▸ (hR r)))
id ┴ └────┘ ┴ └────────────┘ └─────────┘ ┴ ┴ └┘ ┴
src └────┘ └────────────┘ └─────────┘ ┴
typ ┴ └────┘ ┴ └────────────┘ └─────────┘ ┴ ┴ └┘ ┴
349 (λ h, or.inr $ λ r, neg_lt_neg_iff.mp $ lt_of_le_of_lt (neg_le_abs_self _) (h ▸ (hR r)))⟩
id ┴ └────┘ ┴ └────────────┘└─┘ └────────────┘ └─────────────┘ ┴ ┴ └┘ ┴
src └────┘ └────────────┘└─┘ └────────────┘ └─────────────┘ ┴
typ ┴ └────┘ ┴ └────────────┘└─┘ └────────────┘ └─────────────┘ ┴ ┴ └┘ ┴
350
351 lemma infinite_pos_add_not_infinite_neg {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
352 infinite_pos x → ¬ infinite_neg y → infinite_pos (x + y) :=
id └──────────┘ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴ └──────────┘ └──────────┘ ┴
typ └──────────┘ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘ └──────────┘
353 begin
st └─────
354 intros hip hnin r,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └─────────┘
st ──────────────────┘└─
355 cases not_forall.mp hnin with r₂ hr₂,
id └───────────┘ └──┘
src └────┘└───────────┘┴ └──────────┘
typ └────┘└───────────┘┴└──┘└──────────┘
doc └────┘ ┴ └──────────┘
txt └────┘ ┴ └──────────┘
par └────┘ ┴ └──────────┘
pid ┴ ┴ └──────────┘
st ─────────────────────────────────────┘└─
356 convert (add_lt_add_of_lt_of_le (hip (r + -r₂)) (not_lt.mp hr₂)),
id └────────────────────┘ └─┘ ┴ ┴ ┴└┘ └───────┘ └─┘
src └──────┘ └────────────────────┘┴ ┴ ┴┴┴┴ └─┘ └───────┘┴ └┘
typ └──────┘ └────────────────────┘┴ └─┘┴ ┴┴┴┴┴└┘└─┘ └───────┘┴└─┘└┘
doc └──────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
txt └──────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
par └──────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └┘
st ─────────────────────────────────────────────────────────────────┘└─
357 rw [←of_eq_coe, ←of_eq_coe, ←of_eq_coe, of_add, of_neg, ←sub_eq_add_neg, sub_add_cancel]
id └───────┘ └───────┘ └───────┘ └────┘ └────┘ └────────────┘ └────────────┘
src └───┘└───────┘└─┘└───────┘└─┘└───────┘└┘└────┘└┘└────┘└─┘└────────────┘└┘└────────────┘└┘
typ └───┘└───────┘└─┘└───────┘└─┘└───────┘└┘└────┘└┘└────┘└─┘└────────────┘└┘└────────────┘└┘
doc └───┘ └─┘ └─┘ └┘ └┘ └─┘ └┘ └┘
txt └───┘ └─┘ └─┘ └┘ └┘ └─┘ └┘ └┘
par └───┘ └─┘ └─┘ └┘ └┘ └─┘ └┘ └┘
pid └─┘ └─┘ └─┘ └┘ └┘ └─┘ └┘ ┴┴
st ───────────────┘└──────────┘└──────────┘└──────┘└──────┘└───────────────┘└──────────────┘┴┴
358 end
st └─┘
359
360 lemma not_infinite_neg_add_infinite_pos {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
361 ¬ infinite_neg x → infinite_pos y → infinite_pos (x + y) :=
id ┴ └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src ┴ └──────────┘ └──────────┘ └──────────┘ ┴
typ ┴ └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘ └──────────┘
362 λ hx hy, by rw [add_comm]; exact infinite_pos_add_not_infinite_neg hy hx
id └┘ └┘ └──────┘ └───────────────────────────────┘ └┘ └┘
src └──┘└──────┘┴ └────┘└───────────────────────────────┘┴ ┴ └
typ └┘ └┘ └──┘└──────┘┴ └────┘└───────────────────────────────┘┴└┘┴└┘└
doc └──┘ ┴ └────┘ ┴ ┴ └
txt └──┘ ┴ └────┘ ┴ ┴ └
par └──┘ ┴ └────┘ ┴ ┴ └
pid └┘ ┴ ┴ ┴ ┴ └
st └───────────┘┴└───────────────────────────────────────────────
363
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
364 lemma infinite_neg_add_not_infinite_pos {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
365 infinite_neg x → ¬ infinite_pos y → infinite_neg (x + y) :=
id └──────────┘ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴ └──────────┘ └──────────┘ ┴
typ └──────────┘ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘ └──────────┘
366 by rw [@infinite_neg_iff_infinite_pos_neg x, @infinite_pos_iff_infinite_neg_neg y,
id └───────────────────────────────┘ ┴ └───────────────────────────────┘ ┴
src └──┘ └───────────────────────────────┘┴ └┘ └───────────────────────────────┘┴ └─
typ └──┘ └───────────────────────────────┘┴┴└┘ └───────────────────────────────┘┴┴└─
doc └──┘ ┴ └┘ ┴ └─
txt └──┘ ┴ └┘ ┴ └─
par └──┘ ┴ └┘ ┴ └─
pid └┘ ┴ └┘ ┴ └─
st └───────────────────────────────────────┘└────────────────────────────────────┘└─
367 @infinite_neg_iff_infinite_pos_neg (x + y), neg_add];
id └───────────────────────────────┘ ┴ ┴ ┴ └─────┘
src ──────┘ └───────────────────────────────┘┴ ┴┴┴ └─┘└─────┘┴
typ ──────┘ └───────────────────────────────┘┴ ┴┴┴┴┴└─┘└─────┘┴
doc ──────┘ ┴ ┴ ┴ └─┘ ┴
txt ──────┘ ┴ ┴ ┴ └─┘ ┴
par ──────┘ ┴ ┴ ┴ └─┘ ┴
pid ──────┘ ┴ ┴ ┴ └─┘ ┴
st ────────────────────────────────────────────────┘└───────┘┴└─
368 exact infinite_pos_add_not_infinite_neg
id └───────────────────────────────┘
src └────┘└───────────────────────────────┘└
typ └────┘└───────────────────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ────────────────────────────────────────
369
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
370 lemma not_infinite_pos_add_infinite_neg {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
371 ¬ infinite_pos x → infinite_neg y → infinite_neg (x + y) :=
id ┴ └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src ┴ └──────────┘ └──────────┘ └──────────┘ ┴
typ ┴ └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘ └──────────┘
372 λ hx hy, by rw [add_comm]; exact infinite_neg_add_not_infinite_pos hy hx
id └┘ └┘ └──────┘ └───────────────────────────────┘ └┘ └┘
src └──┘└──────┘┴ └────┘└───────────────────────────────┘┴ ┴ └
typ └┘ └┘ └──┘└──────┘┴ └────┘└───────────────────────────────┘┴└┘┴└┘└
doc └──┘ ┴ └────┘ ┴ ┴ └
txt └──┘ ┴ └────┘ ┴ ┴ └
par └──┘ ┴ └────┘ ┴ ┴ └
pid └┘ ┴ ┴ ┴ ┴ └
st └───────────┘┴└───────────────────────────────────────────────
373
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
374 lemma infinite_pos_add_infinite_pos {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
375 infinite_pos x → infinite_pos y → infinite_pos (x + y) :=
id └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ └──────────┘ └──────────┘ ┴
typ └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘ └──────────┘
376 λ hx hy, infinite_pos_add_not_infinite_neg hx (not_infinite_neg_of_infinite_pos hy)
id └┘ └┘ └───────────────────────────────┘ └┘ └──────────────────────────────┘ └┘
src └───────────────────────────────┘ └──────────────────────────────┘
typ └┘ └┘ └───────────────────────────────┘ └┘ └──────────────────────────────┘ └┘
377
378 lemma infinite_neg_add_infinite_neg {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
379 infinite_neg x → infinite_neg y → infinite_neg (x + y) :=
id └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ └──────────┘ └──────────┘ ┴
typ └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘ └──────────┘
380 λ hx hy, infinite_neg_add_not_infinite_pos hx (not_infinite_pos_of_infinite_neg hy)
id └┘ └┘ └───────────────────────────────┘ └┘ └──────────────────────────────┘ └┘
src └───────────────────────────────┘ └──────────────────────────────┘
typ └┘ └┘ └───────────────────────────────┘ └┘ └──────────────────────────────┘ └┘
381
382 lemma infinite_pos_add_not_infinite {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
383 infinite_pos x → ¬ infinite y → infinite_pos (x + y) :=
id └──────────┘ ┴ ┴ └──────┘ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴ └──────┘ └──────────┘ ┴
typ └──────────┘ ┴ ┴ └──────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────┘ └──────────┘
384 λ hx hy, infinite_pos_add_not_infinite_neg hx (not_or_distrib.mp hy).2
id └┘ └┘ └───────────────────────────────┘ └┘ └────────────┘└─┘ └┘ ┴
src └───────────────────────────────┘ └────────────┘└─┘ ┴
typ └┘ └┘ └───────────────────────────────┘ └┘ └────────────┘└─┘ └┘ ┴
385
386 lemma infinite_neg_add_not_infinite {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
387 infinite_neg x → ¬ infinite y → infinite_neg (x + y) :=
id └──────────┘ ┴ ┴ └──────┘ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴ └──────┘ └──────────┘ ┴
typ └──────────┘ ┴ ┴ └──────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────┘ └──────────┘
388 λ hx hy, infinite_neg_add_not_infinite_pos hx (not_or_distrib.mp hy).1
id └┘ └┘ └───────────────────────────────┘ └┘ └────────────┘└─┘ └┘ ┴
src └───────────────────────────────┘ └────────────┘└─┘ ┴
typ └┘ └┘ └───────────────────────────────┘ └┘ └────────────┘└─┘ └┘ ┴
389
390 theorem infinite_pos_of_tendsto_top {f : ℕ → ℝ} (hf : tendsto f at_top at_top) :
id ┴ ┴ └─────┘ ┴ └────┘ └────┘
src ┴ ┴ └─────┘ └────┘ └────┘
typ ┴ ┴ └─────┘ ┴ └────┘ └────┘
doc └─────┘ └────┘ └────┘
391 infinite_pos (of_seq f) :=
id └──────────┘ └────┘ ┴
src └──────────┘ └────┘
typ └──────────┘ └────┘ ┴
doc └──────────┘
392 λ r, have hf' : _ := (tendsto_at_top_at_top _).mp hf,
id ┴ └───────────────────┘ └┘ └┘
src └───────────────────┘ └┘
typ ┴ └───────────────────┘ └┘ └┘
393 Exists.cases_on (hf' (r + 1)) $ λ i hi,
id └─────────────┘ └─┘ ┴ ┴ ┴ └┘
src └─────────────┘ ┴
typ └─────────────┘ └─┘ ┴ ┴ ┴ └┘
394 have hi' : ∀ (a : ℕ), f a < (r + 1) → a < i :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
395 λ a, by rw [←not_le, ←not_le]; exact not_imp_not.mpr (hi a),
id ┴ └────┘ └────┘ └─────────────┘ └┘ ┴
src └───┘└────┘└─┘└────┘┴ └────┘└─────────────┘┴ ┴ ┴
typ ┴ └───┘└────┘└─┘└────┘┴ └────┘└─────────────┘┴ └┘┴┴┴
doc └───┘ └─┘ ┴ └────┘ ┴ ┴ ┴
txt └───┘ └─┘ ┴ └────┘ ┴ ┴ ┴
par └───┘ └─┘ ┴ └────┘ ┴ ┴ ┴
pid └─┘ └─┘ ┴ ┴ ┴ ┴ ┴
st └──────────┘└───────┘┴└────────────────────────────┘
396 have hS : - {a : ℕ | r < f a} ⊆ {a : ℕ | a ≤ i} :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
397 by simp only [set.compl_set_of, not_lt];
id └──────────────┘ └────┘
src └─────────┘└──────────────┘└┘└────┘┴
typ └─────────┘└──────────────┘└┘└────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └──────────────────────────────────────
398 exact λ a har, le_of_lt (hi' a (lt_of_le_of_lt har (lt_add_one _))),
id └──────┘ └─┘ └────────────┘ └────────┘
src └────┘ └──────┘└──────┘┴ ┴ ┴ └────────────┘┴ ┴ └────────┘└───┘
typ └────┘ └──────┘└──────┘┴ └─┘┴ ┴ └────────────┘┴ ┴ └────────┘└───┘
doc └────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └───┘
txt └────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └───┘
par └────┘ └──────┘ ┴ ┴ ┴ ┴ ┴ └───┘
pid ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └───┘
st ──────────────────────────────────────────────────────────────────────┘
399 (lt_def U).mpr $ mem_hyperfilter_of_finite_compl $
id └────┘ ┴ └─┘ └─────────────────────────────┘
src └────┘ ┴ └─┘ └─────────────────────────────┘
typ └────┘ ┴ └─┘ └─────────────────────────────┘
400 set.finite_subset (set.finite_le_nat _) hS
id └───────────────┘ └───────────────┘ └┘
src └───────────────┘ └───────────────┘
typ └───────────────┘ └───────────────┘ └┘
401
402 theorem infinite_neg_of_tendsto_bot {f : ℕ → ℝ} (hf : tendsto f at_top at_bot) :
id ┴ ┴ └─────┘ ┴ └────┘ └────┘
src ┴ ┴ └─────┘ └────┘ └────┘
typ ┴ ┴ └─────┘ ┴ └────┘ └────┘
doc └─────┘ └────┘ └────┘
403 infinite_neg (of_seq f) :=
id └──────────┘ └────┘ ┴
src └──────────┘ └────┘
typ └──────────┘ └────┘ ┴
doc └──────────┘
404 λ r, have hf' : _ := (tendsto_at_top_at_bot _).mp hf,
id ┴ └───────────────────┘ └┘ └┘
src └───────────────────┘ └┘
typ ┴ └───────────────────┘ └┘ └┘
405 Exists.cases_on (hf' (r - 1)) $ λ i hi,
id └─────────────┘ └─┘ ┴ ┴ ┴ └┘
src └─────────────┘ ┴
typ └─────────────┘ └─┘ ┴ ┴ ┴ └┘
406 have hi' : ∀ (a : ℕ), r - 1 < f a → a < i :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
407 λ a, by rw [←not_le, ←not_le]; exact not_imp_not.mpr (hi a),
id ┴ └────┘ └────┘ └─────────────┘ └┘ ┴
src └───┘└────┘└─┘└────┘┴ └────┘└─────────────┘┴ ┴ ┴
typ ┴ └───┘└────┘└─┘└────┘┴ └────┘└─────────────┘┴ └┘┴┴┴
doc └───┘ └─┘ ┴ └────┘ ┴ ┴ ┴
txt └───┘ └─┘ ┴ └────┘ ┴ ┴ ┴
par └───┘ └─┘ ┴ └────┘ ┴ ┴ ┴
pid └─┘ └─┘ ┴ ┴ ┴ ┴ ┴
st └──────────┘└───────┘┴└────────────────────────────┘
408 have hS : - {a : ℕ | f a < r} ⊆ {a : ℕ | a ≤ i} :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
409 by simp only [set.compl_set_of, not_lt];
id └──────────────┘ └────┘
src └─────────┘└──────────────┘└┘└────┘┴
typ └─────────┘└──────────────┘└┘└────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └──────────────────────────────────────
410 exact λ a har, le_of_lt (hi' a (lt_of_lt_of_le (sub_one_lt _) har)),
id └──────┘ └─┘ └────────────┘ └────────┘
src └────┘ └──────┘└──────┘┴ ┴ ┴ └────────────┘┴ └────────┘└──┘ └┘
typ └────┘ └──────┘└──────┘┴ └─┘┴ ┴ └────────────┘┴ └────────┘└──┘ └┘
doc └────┘ └──────┘ ┴ ┴ ┴ ┴ └──┘ └┘
txt └────┘ └──────┘ ┴ ┴ ┴ ┴ └──┘ └┘
par └────┘ └──────┘ ┴ ┴ ┴ ┴ └──┘ └┘
pid ┴ └──────┘ ┴ ┴ ┴ ┴ └──┘ └┘
st ──────────────────────────────────────────────────────────────────────┘
411 (lt_def U).mpr $ mem_hyperfilter_of_finite_compl $
id └────┘ ┴ └─┘ └─────────────────────────────┘
src └────┘ ┴ └─┘ └─────────────────────────────┘
typ └────┘ ┴ └─┘ └─────────────────────────────┘
412 set.finite_subset (set.finite_le_nat _) hS
id └───────────────┘ └───────────────┘ └┘
src └───────────────┘ └───────────────┘
typ └───────────────┘ └───────────────┘ └┘
413
414 lemma not_infinite_neg {x : ℝ*} : ¬ infinite x → ¬ infinite (-x) :=
id └┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴┴
src └┘ ┴ └──────┘ ┴ └──────┘ ┴
typ └┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴┴
doc └┘ └──────┘ └──────┘
415 not_imp_not.mpr infinite_iff_infinite_neg.mpr
id └─────────┘└──┘ └───────────────────────┘└──┘
src └─────────┘└──┘ └───────────────────────┘└──┘
typ └─────────┘└──┘ └───────────────────────┘└──┘
416
417 lemma not_infinite_add {x y : ℝ*} (hx : ¬ infinite x) (hy : ¬ infinite y) :
id └┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └┘ ┴ └──────┘ ┴ └──────┘
typ └┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴
doc └┘ └──────┘ └──────┘
418 ¬ infinite (x + y) :=
id ┴ └──────┘ ┴ ┴ ┴
src ┴ └──────┘ ┴
typ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘
419 have hx' : _ := exists_st_of_not_infinite hx, have hy' : _ := exists_st_of_not_infinite hy,
id └───────────────────────┘ └┘ └───────────────────────┘ └┘
src └───────────────────────┘ └───────────────────────┘
typ └───────────────────────┘ └┘ └───────────────────────┘ └┘
420 Exists.cases_on hx' $ Exists.cases_on hy' $
id └─────────────┘ └─┘ └─────────────┘ └─┘
src └─────────────┘ └─────────────┘
typ └─────────────┘ └─┘ └─────────────┘ └─┘
421 λ r hr s hs, not_infinite_of_exists_st $ ⟨s + r, is_st_add hs hr⟩
id ┴ └┘ ┴ └┘ └───────────────────────┘ ┴ ┴ ┴ └───────┘ └┘ └┘
src └───────────────────────┘ ┴ └───────┘
typ ┴ └┘ ┴ └┘ └───────────────────────┘ ┴ ┴ ┴ └───────┘ └┘ └┘
422
423 theorem not_infinite_iff_exist_lt_gt {x : ℝ*} : ¬ infinite x ↔ ∃ r s : ℝ, (r : ℝ*) < x ∧ x < s :=
id └┘ ┴ └──────┘ ┴ ┴ ┴ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └──────┘ ┴ ┴ ┴┴ └┘ ┴ ┴ ┴
typ └┘ ┴ └──────┘ ┴ ┴ ┴ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └──────┘ └┘
424 ⟨ λ hni,
id └─┘
typ └─┘
425 Exists.dcases_on (not_forall.mp (not_or_distrib.mp hni).1) $
id └──────────────┘ └────────┘└─┘ └────────────┘└─┘ └─┘ ┴
src └──────────────┘ └────────┘└─┘ └────────────┘└─┘ ┴
typ └──────────────┘ └────────┘└─┘ └────────────┘└─┘ └─┘ ┴
426 Exists.dcases_on (not_forall.mp (not_or_distrib.mp hni).2) $ λ r hr s hs,
id └──────────────┘ └────────┘└─┘ └────────────┘└─┘ └─┘ ┴ ┴ └┘ ┴ └┘
src └──────────────┘ └────────┘└─┘ └────────────┘└─┘ ┴
typ └──────────────┘ └────────┘└─┘ └────────────┘└─┘ └─┘ ┴ ┴ └┘ ┴ └┘
427 by rw [not_lt] at hr hs; exact ⟨r - 1, s + 1,
id └────┘ ┴ ┴ ┴ ┴
src └──┘└────┘└────────┘ └────┘ ┴┴└──┘ ┴┴└───
typ └──┘└────┘└────────┘ └────┘ ┴┴┴└──┘┴┴┴└───
doc └──┘ └────────┘ └────┘ ┴ └──┘ ┴ └───
txt └──┘ └────────┘ └────┘ ┴ └──┘ ┴ └───
par └──┘ └────────┘ └────┘ ┴ └──┘ ┴ └───
pid └┘ ┴└───────┘ ┴ ┴ └──┘ ┴ └───
st └─────────┘┴└───────────────────────────────
428 ⟨ lt_of_lt_of_le (by rw [←of_eq_coe, of_sub]; exact sub_one_lt _) hr,
id └────────────┘ └───────┘ └────┘ └────────┘ └┘
src ─┘ ┴└────────────┘┴ ┴└───┘└───────┘└┘└────┘┴└──────┘└────────┘└──┘ └─
typ ─┘ ┴└────────────┘┴ ┴└───┘└───────┘└┘└────┘┴└──────┘└────────┘└──┘└┘└─
doc ─┘ ┴ ┴ ┴└───┘ └┘ ┴└──────┘ └──┘ └─
txt ─┘ ┴ ┴ ┴└───┘ └┘ ┴└──────┘ └──┘ └─
par ─┘ ┴ ┴ ┴└───┘ └┘ ┴└──────┘ └──┘ └─
pid ─┘ ┴ ┴ └────┘ └┘ └───────┘ └──┘ └─
st ─────────────────────┘└─────────────┘└──────┘┴└──────────────────┘└─────
429 lt_of_le_of_lt hs (by rw [←of_eq_coe (s + 1), of_add]; exact lt_add_one _)⟩ ⟩,
id └────────────┘ └┘ └───────┘ ┴ └────┘ └────────┘
src ───┘└────────────┘┴ ┴ ┴└───┘└───────┘┴ ┴ └───┘└────┘┴└──────┘└────────┘└────┘
typ ───┘└────────────┘┴└┘┴ ┴└───┘└───────┘┴ ┴┴ └───┘└────┘┴└──────┘└────────┘└────┘
doc ───┘ ┴ ┴ ┴└───┘ ┴ ┴ └───┘ ┴└──────┘ └────┘
txt ───┘ ┴ ┴ ┴└───┘ ┴ ┴ └───┘ ┴└──────┘ └────┘
par ───┘ ┴ ┴ ┴└───┘ ┴ ┴ └───┘ ┴└──────┘ └────┘
pid ───┘ ┴ ┴ └────┘ ┴ ┴ └───┘ └───────┘ └────┘
st ────────────────────────┘└─────────────────────┘└──────┘┴└──────────────────┘└──┘
430 λ hrs, Exists.dcases_on hrs $ λ r hr, Exists.dcases_on hr $ λ s hs,
id └─┘ └──────────────┘ └─┘ ┴ └┘ └──────────────┘ └┘ ┴ └┘
src └──────────────┘ └──────────────┘
typ └─┘ └──────────────┘ └─┘ ┴ └┘ └──────────────┘ └┘ ┴ └┘
431 not_or_distrib.mpr ⟨not_forall.mpr ⟨s, lt_asymm (hs.2)⟩, not_forall.mpr ⟨r, lt_asymm (hs.1) ⟩⟩⟩
id └────────────┘└──┘ └────────┘└──┘ ┴ └──────┘ └┘┴ └────────┘└──┘ ┴ └──────┘ └┘┴
src └────────────┘└──┘ └────────┘└──┘ └──────┘ ┴ └────────┘└──┘ └──────┘ ┴
typ └────────────┘└──┘ └────────┘└──┘ ┴ └──────┘ └┘┴ └────────┘└──┘ ┴ └──────┘ └┘┴
432
433 theorem not_infinite_real (r : ℝ) : ¬ infinite r := by rw not_infinite_iff_exist_lt_gt; exact
id ┴ ┴ └──────┘ ┴ └──────────────────────────┘
src ┴ ┴ └──────┘ └─┘└──────────────────────────┘ └────┘
typ ┴ ┴ └──────┘ ┴ └─┘└──────────────────────────┘ └────┘
doc └──────┘ └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └───────────────────────────────────────
434 ⟨ r - 1, r + 1,
id ┴ ┴ ┴
src ┴ ┴┴└──┘ ┴┴└───
typ ┴ ┴┴└──┘┴┴┴└───
doc ┴ ┴ └──┘ ┴ └───
txt ┴ ┴ └──┘ ┴ └───
par ┴ ┴ └──┘ ┴ └───
pid ┴ ┴ └──┘ ┴ └───
st ────────────────
435 by rw [←of_eq_coe, ←of_eq_coe, ←of_lt U]; exact sub_one_lt _,
id └───────┘ └───────┘ └───┘ ┴ └────────┘
src ─┘ ┴└───┘└───────┘└─┘└───────┘└─┘└───┘┴┴┴└──────┘└────────┘└───
typ ─┘ ┴└───┘└───────┘└─┘└───────┘└─┘└───┘┴┴┴└──────┘└────────┘└───
doc ─┘ ┴└───┘ └─┘ └─┘ ┴ ┴└──────┘ └───
txt ─┘ ┴└───┘ └─┘ └─┘ ┴ ┴└──────┘ └───
par ─┘ ┴└───┘ └─┘ └─┘ ┴ ┴└──────┘ └───
pid ─┘ └────┘ └─┘ └─┘ ┴ └───────┘ └───
st ───┘└─────────────┘└──────────┘└────────┘┴└──────────────────┘└─
436 by rw [←of_eq_coe, ←of_eq_coe, ←of_lt U]; exact lt_add_one _⟩
id └───────┘ └───────┘ └───┘ ┴ └────────┘
src ─┘ ┴└───┘└───────┘└─┘└───────┘└─┘└───┘┴┴┴└──────┘└────────┘└───
typ ─┘ ┴└───┘└───────┘└─┘└───────┘└─┘└───┘┴┴┴└──────┘└────────┘└───
doc ─┘ ┴└───┘ └─┘ └─┘ ┴ ┴└──────┘ └───
txt ─┘ ┴└───┘ └─┘ └─┘ ┴ ┴└──────┘ └───
par ─┘ ┴└───┘ └─┘ └─┘ ┴ ┴└──────┘ └───
pid ─┘ └────┘ └─┘ └─┘ ┴ └───────┘ └─┘└
st ───┘└─────────────┘└──────────┘└────────┘┴└──────────────────┘└─
437
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
438 theorem not_real_of_infinite {x : ℝ*} : infinite x → ∀ r : ℝ, x ≠ of r :=
id └┘ └──────┘ ┴ ┴ ┴ ┴ └┘ ┴
src └┘ └──────┘ ┴ ┴ └┘
typ └┘ └──────┘ ┴ ┴ ┴ ┴ └┘ ┴
doc └┘ └──────┘ └┘
439 λ hi r hr, not_infinite_real r $ @eq.subst _ infinite _ _ hr hi
id └┘ ┴ └┘ └───────────────┘ ┴ └──────┘ └──────┘ └┘ └┘
src └───────────────┘ └──────┘ └──────┘
typ └┘ ┴ └┘ └───────────────┘ ┴ └──────┘ └──────┘ └┘ └┘
doc └──────┘
440
441 -- FACTS ABOUT ST THAT REQUIRE SOME INFINITE MACHINERY
442
443 private lemma is_st_mul' {x y : ℝ*} {r s : ℝ} (hxr : is_st x r) (hys : is_st y s) (hs : s ≠ 0) :
id └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
src └┘ ┴ └───┘ └───┘ ┴
typ └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴
doc └┘ └───┘ └───┘
444 is_st (x * y) (r * s) :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
445 have hxr' : _ := is_st_iff_abs_sub_lt_delta.mp hxr,
id └────────────────────────┘└─┘ └─┘
src └────────────────────────┘└─┘
typ └────────────────────────┘└─┘ └─┘
446 have hys' : _ := is_st_iff_abs_sub_lt_delta.mp hys,
id └────────────────────────┘└─┘ └─┘
src └────────────────────────┘└─┘
typ └────────────────────────┘└─┘ └─┘
447 have h : _ := not_infinite_iff_exist_lt_gt.mp $ not_imp_not.mpr infinite_iff_infinite_abs.mpr $
id └──────────────────────────┘└─┘ └─────────┘└──┘ └───────────────────────┘└──┘
src └──────────────────────────┘└─┘ └─────────┘└──┘ └───────────────────────┘└──┘
typ └──────────────────────────┘└─┘ └─────────┘└──┘ └───────────────────────┘└──┘
448 not_infinite_of_exists_st ⟨r, hxr⟩,
id └───────────────────────┘ ┴ └─┘
src └───────────────────────┘
typ └───────────────────────┘ ┴ └─┘
449 Exists.cases_on h $ λ u h', Exists.cases_on h' $ λ t ⟨hu, ht⟩,
id └─────────────┘ ┴ ┴ └┘ └─────────────┘ └┘ ┴ ┴ └┘
src └─────────────┘ └─────────────┘
typ └─────────────┘ ┴ ┴ └┘ └─────────────┘ └┘ ┴ ┴ └┘
450 is_st_iff_abs_sub_lt_delta.mpr $ λ d hd,
id └────────────────────────┘└──┘ ┴ └┘
src └────────────────────────┘└──┘
typ └────────────────────────┘└──┘ ┴ └┘
451 calc abs (x * y - of (r * s))
id └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └─┘ ┴ ┴ └┘ ┴
typ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └┘
452 = abs (x * y - (of r) * (of s)) : by rw of_mul
id └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └────┘
src └─┘ ┴ ┴ └┘ ┴ └┘ └─┘└────┘└
typ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─┘└────┘└
doc └┘ └┘ └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └┘ └──────────
453 ... = abs (x * (y - of s) + (x - of r) * (of s)) :
id └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src ─┘ └─┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └┘
typ ─┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc ─┘ └┘ └┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
454 by rw [mul_sub, sub_mul, add_sub, sub_add_cancel]
id └─────┘ └─────┘ └─────┘ └────────────┘
src └──┘└─────┘└┘└─────┘└┘└─────┘└┘└────────────┘└─
typ └──┘└─────┘└┘└─────┘└┘└─────┘└┘└────────────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ ┴└
st └──────────┘└───────┘└───────┘└──────────────┘┴└
455 ... ≤ abs (x * (y - of s)) + abs ((x - of r) * (of s)) : abs_add _ _
id └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─────┘
src ─┘ └─┘ ┴ ┴ └┘ ┴ └─┘ ┴ └┘ ┴ └┘ └─────┘
typ ─┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └─────┘
doc ─┘ └┘ └┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
456 ... ≤ abs x * abs (y - of s) + abs (x - of r) * abs (of s) : by simp only [abs_mul]
id └─┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └─────┘
src └─┘ ┴ └─┘ ┴ └┘ ┴ └─┘ ┴ └┘ ┴ └─┘ └┘ └─────────┘└─────┘└─
typ └─┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └─────────┘└─────┘└─
doc └┘ └┘ └┘ └─────────┘ └─
txt └─────────┘ └─
par └─────────┘ └─
pid ┴└──┘└┘ ┴└
st └────────────────────
457 ... ≤ abs x * of ((d / t) / 2) + of ((d / abs s) / 2) * abs (of s) : add_le_add
id └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ └┘ ┴ └────────┘
src ─┘ └─┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └─┘ └┘ └────────┘
typ ─┘ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ └┘ ┴ └────────┘
doc ─┘ └┘ └┘ └┘
txt ─┘
par ─┘
pid ─┘
st ─┘
458 (mul_le_mul_of_nonneg_left (le_of_lt $ hys' _ $ half_pos $ div_pos hd $
id └───────────────────────┘ └──────┘ └──┘ └──────┘ └─────┘ └┘
src └───────────────────────┘ └──────┘ └──────┘ └─────┘
typ └───────────────────────┘ └──────┘ └──┘ └──────┘ └─────┘ └┘
459 (of_lt U).mpr $ lt_of_le_of_lt (abs_nonneg _) ht) $ abs_nonneg _ )
id └───┘ ┴ └─┘ └────────────┘ └────────┘ └────────┘
src └───┘ ┴ └─┘ └────────────┘ └────────┘ └────────┘
typ └───┘ ┴ └─┘ └────────────┘ └────────┘ └────────┘
460 (mul_le_mul_of_nonneg_right (le_of_lt $ hxr' _ $ half_pos $ div_pos hd $
id └────────────────────────┘ └──────┘ └──┘ └──────┘ └─────┘ └┘
src └────────────────────────┘ └──────┘ └──────┘ └─────┘
typ └────────────────────────┘ └──────┘ └──┘ └──────┘ └─────┘ └┘
461 abs_pos_of_ne_zero hs) $ abs_nonneg _)
id └────────────────┘ └┘ └────────┘
src └────────────────┘ └────────┘
typ └────────────────┘ └┘ └────────┘
462 ... = (of d) / 2 * (abs x / of t) + ((of d) / 2) : by
id └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └┘ ┴ ┴ └─┘ ┴ └┘ ┴ └┘ ┴
typ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └┘ └┘ └┘
st └
463 { rw [div_div_eq_div_mul, mul_comm t 2, ←div_div_eq_div_mul,
id └────────────────┘ └──────┘ ┴ └────────────────┘
src └──┘└────────────────┘└┘└──────┘┴ └───┘└────────────────┘└─
typ └──┘└────────────────┘└┘└──────┘┴┴└───┘└────────────────┘└─
doc └──┘ └┘ ┴ └───┘ └─
txt └──┘ └┘ ┴ └───┘ └─
par └──┘ └┘ ┴ └───┘ └─
pid └┘ └┘ ┴ └───┘ └─
st ─────────────────────────────┘└───────────┘└────────────────────┘└─
464 of_div U, div_div_eq_div_mul, mul_comm (abs s) 2,
id └────┘ ┴ └────────────────┘ └──────┘ └─┘ ┴
src ───────────┘└────┘┴┴└┘└────────────────┘└┘└──────┘┴ └─┘┴ └────
typ ───────────┘└────┘┴┴└┘└────────────────┘└┘└──────┘┴ └─┘┴┴└────
doc ───────────┘ ┴ └┘ └┘ ┴ ┴ └────
txt ───────────┘ ┴ └┘ └┘ ┴ ┴ └────
par ───────────┘ ┴ └┘ └┘ ┴ ┴ └────
pid ───────────┘ ┴ └┘ └┘ ┴ ┴ └────
st ───────────────────┘└──────────────────┘└─────────────────┘└──
465 ←div_div_eq_div_mul, mul_div_comm, of_div U, of_div U, of_div U, of_abs U,
id └────────────────┘ └──────────┘ └────┘ ┴ └────┘ ┴ └────┘ ┴ └────┘ ┴
src ────────┘└────────────────┘└┘└──────────┘└┘└────┘┴┴└┘└────┘┴┴└┘└────┘┴┴└┘└────┘┴┴└─
typ ────────┘└────────────────┘└┘└──────────┘└┘└────┘┴┴└┘└────┘┴┴└┘└────┘┴┴└┘└────┘┴┴└─
doc ────────┘ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └─
txt ────────┘ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └─
par ────────┘ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └─
pid ────────┘ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └─
st ──────────────────────────┘└────────────┘└────────┘└────────┘└────────┘└────────┘└─
466 div_mul_cancel _ (ne_of_gt (abs_pos_of_ne_zero ((of_ne_zero U.1 _).mp hs)))], refl }
id └────────────┘ └──────┘ └────────────────┘ └────────┘ ┴ └┘
src ───────┘└────────────┘└─┘ └──────┘┴ └────────────────┘┴ └────────┘┴┴└───────┘ └──┘ └───┘
typ ───────┘└────────────┘└─┘ └──────┘┴ └────────────────┘┴ └────────┘┴┴└───────┘└┘└──┘ └───┘
doc ───────┘ └─┘ ┴ ┴ ┴ └───────┘ └──┘ └───┘
txt ───────┘ └─┘ ┴ ┴ ┴ └───────┘ └──┘ └───┘
par ───────┘ └─┘ ┴ ┴ ┴ └───────┘ └──┘ └───┘
pid ───────┘ └─┘ ┴ ┴ ┴ └───────┘ └──┘ ┴
st ──────────────────────────────────────────────────────────────────────────────────┘└──────┘└┘
467 ... < (of d) / 2 * 1 + ((of d) / 2) :
id └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └┘ ┴ ┴ ┴ └┘ ┴
typ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
doc └┘ └┘
468 add_lt_add_right (mul_lt_mul_of_pos_left
id └──────────────┘ └────────────────────┘
src └──────────────┘ └────────────────────┘
typ └──────────────┘ └────────────────────┘
469 ((div_lt_one_iff_lt $ lt_of_le_of_lt (abs_nonneg x) ht).mpr ht) $
id └───────────────┘ └────────────┘ └────────┘ ┴ └─┘
src └───────────────┘ └────────────┘ └────────┘ └─┘
typ └───────────────┘ └────────────┘ └────────┘ ┴ └─┘
470 half_pos $ of_lt_of_lt U hd) _
id └──────┘ └─────────┘ ┴ └┘
src └──────┘ └─────────┘ ┴
typ └──────┘ └─────────┘ ┴ └┘
471 ... = of d : by rw [mul_one, add_halves]
id └┘ ┴ └─────┘ └────────┘
src └┘ └──┘└─────┘└┘└────────┘└─
typ └┘ ┴ └──┘└─────┘└┘└────────┘└─
doc └┘ └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └──────────┘└──────────┘┴└
472
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
473 lemma is_st_mul {x y : ℝ*} {r s : ℝ} (hxr : is_st x r) (hys : is_st y s) :
id └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴
src └┘ ┴ └───┘ └───┘
typ └┘ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴
doc └┘ └───┘ └───┘
474 is_st (x * y) (r * s) :=
id └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴
typ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───┘
475 have h : _ := not_infinite_iff_exist_lt_gt.mp $
id └──────────────────────────┘└─┘
src └──────────────────────────┘└─┘
typ └──────────────────────────┘└─┘
476 not_imp_not.mpr infinite_iff_infinite_abs.mpr $ not_infinite_of_exists_st ⟨r, hxr⟩,
id └─────────┘└──┘ └───────────────────────┘└──┘ └───────────────────────┘ ┴ └─┘
src └─────────┘└──┘ └───────────────────────┘└──┘ └───────────────────────┘
typ └─────────┘└──┘ └───────────────────────┘└──┘ └───────────────────────┘ ┴ └─┘
477 Exists.cases_on h $ λ u h', Exists.cases_on h' $ λ t ⟨hu, ht⟩,
id └─────────────┘ ┴ ┴ └┘ └─────────────┘ └┘ ┴ ┴
src └─────────────┘ └─────────────┘
typ └─────────────┘ ┴ ┴ └┘ └─────────────┘ └┘ ┴ ┴
478 begin
st └─────
479 by_cases hs : s = 0,
id ┴ ┴
src └───────┘ └─┘ ┴┴└┘
typ └───────┘ └─┘┴┴┴└┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ────────────────────┘└─
480 { apply is_st_iff_abs_sub_lt_delta.mpr, intros d hd,
src └────┘ └─────────┘
typ └────┘ └─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └───┘
st ───┘└──────────────────────────────────┘└───────────┘└─
481 have hys' : _ := is_st_iff_abs_sub_lt_delta.mp hys (d / t)
id └───────────────────────────┘ └─┘ ┴ ┴ ┴
src └───────────────┘└───────────────────────────┘┴ ┴ ┴┴┴ └─
typ └───────────────┘└───────────────────────────┘┴└─┘┴ ┴┴┴┴┴└─
doc └───────────────┘ ┴ ┴ ┴ ┴ └─
txt └───────────────┘ ┴ ┴ ┴ ┴ └─
par └───────────────┘ ┴ ┴ ┴ ┴ └─
pid └───────┘└──┘└──┘ ┴ ┴ ┴ ┴ └─
st ───────────────────────────────────────────────────────────────
482 (div_pos hd ((of_lt U).mpr (lt_of_le_of_lt (abs_nonneg x) ht))),
id └─────┘ └┘ └───┘ ┴ └────────────┘ └────────┘ ┴ └┘
src ─────┘ └─────┘┴ ┴ └───┘┴┴└────┘ └────────────┘┴ └────────┘┴ └┘ └─┘
typ ─────┘ └─────┘┴└┘┴ └───┘┴┴└────┘ └────────────┘┴ └────────┘┴┴└┘└┘└─┘
doc ─────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └┘ └─┘
txt ─────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └┘ └─┘
par ─────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └┘ └─┘
pid ─────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └┘ └─┘
st ────────────────────────────────────────────────────────────────────┘└─
483 rw [hs, ←of_eq_coe _, of_zero, sub_zero] at hys',
id └┘ └───────┘ └─────┘ └──────┘
src └──┘ └─┘└───────┘└──┘└─────┘└┘└──────┘└───────┘
typ └──┘└┘└─┘└───────┘└──┘└─────┘└┘└──────┘└───────┘
doc └──┘ └─┘ └──┘ └┘ └───────┘
txt └──┘ └─┘ └──┘ └┘ └───────┘
par └──┘ └─┘ └──┘ └┘ └───────┘
pid └┘ └─┘ └──┘ └┘ ┴└──────┘
st ─────────┘└────────────┘└───────┘└────────┘┴└──────┘└─
484 rw [hs, mul_zero, (of_eq_coe _).symm, of_zero, sub_zero, abs_mul, mul_comm,
id └┘ └──────┘ └───────┘ └─────┘ └──────┘ └─────┘ └──────┘
src └──┘ └┘└──────┘└┘ └───────┘└────────┘└─────┘└┘└──────┘└┘└─────┘└┘└──────┘└─
typ └──┘└┘└┘└──────┘└┘ └───────┘└────────┘└─────┘└┘└──────┘└┘└─────┘└┘└──────┘└─
doc └──┘ └┘ └┘ └────────┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └────────┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └────────┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └────────┘ └┘ └┘ └┘ └─
st ─────────┘└────────┘└─────────────────┘└────────┘└────────┘└───────┘└────────┘└─
485 ←div_mul_cancel (d : ℝ*) (ne_of_gt (lt_of_le_of_lt (abs_nonneg x) ht)),
id └────────────┘ ┴ └──────┘ └────────────┘ └────────┘ ┴ └┘
src ────────┘└────────────┘┴ └─┘ └┘ └──────┘┴ └────────────┘┴ └────────┘┴ └┘ └───
typ ────────┘└────────────┘┴ ┴└─┘ └┘ └──────┘┴ └────────────┘┴ └────────┘┴┴└┘└┘└───
doc ────────┘ ┴ └─┘ └┘ ┴ ┴ ┴ └┘ └───
txt ────────┘ ┴ └─┘ └┘ ┴ ┴ ┴ └┘ └───
par ────────┘ ┴ └─┘ └┘ ┴ ┴ ┴ └┘ └───
pid ────────┘ ┴ └─┘ └┘ ┴ ┴ ┴ └┘ └───
st ─────────────────────────────────────────────────────────────────────────────┘└─
486 ←of_eq_coe d, ←of_eq_coe t, ←of_div U],
id └───────┘ ┴ └───────┘ ┴ └────┘ ┴
src ────────┘└───────┘┴ └─┘└───────┘┴ └─┘└────┘┴┴┴
typ ────────┘└───────┘┴┴└─┘└───────┘┴┴└─┘└────┘┴┴┴
doc ────────┘ ┴ └─┘ ┴ └─┘ ┴ ┴
txt ────────┘ ┴ └─┘ ┴ └─┘ ┴ ┴
par ────────┘ ┴ └─┘ ┴ └─┘ ┴ ┴
pid ────────┘ ┴ └─┘ ┴ └─┘ ┴ ┴
st ───────────────────┘└────────────┘└─────────┘└──
487 exact mul_lt_mul'' hys' ht (abs_nonneg _) (abs_nonneg _) },
id └──────────┘ └──┘ └┘ └────────┘
src └────┘└──────────┘┴ ┴ ┴ └──┘ └────────┘└──┘
typ └────┘└──────────┘┴└──┘┴└┘┴ └──┘ └────────┘└──┘
doc └────┘ ┴ ┴ ┴ └──┘ └──┘
txt └────┘ ┴ ┴ ┴ └──┘ └──┘
par └────┘ ┴ ┴ ┴ └──┘ └──┘
pid ┴ ┴ ┴ ┴ └──┘ └─┘┴
st ────────────────────────────────────────────────────────────┘└┘└
488 exact is_st_mul' hxr hys hs,
id └────────┘ └─┘ └─┘ └┘
src └────┘└────────┘┴ ┴ ┴
typ └────┘└────────┘┴└─┘┴└─┘┴└┘
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────────┘└─
489 end
st ──┘
490
491 --AN INFINITE LEMMA THAT REQUIRES SOME MORE ST MACHINERY
492 lemma not_infinite_mul {x y : ℝ*} (hx : ¬ infinite x) (hy : ¬ infinite y) :
id └┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └┘ ┴ └──────┘ ┴ └──────┘
typ └┘ ┴ └──────┘ ┴ ┴ └──────┘ ┴
doc └┘ └──────┘ └──────┘
493 ¬ infinite (x * y) :=
id ┴ └──────┘ ┴ ┴ ┴
src ┴ └──────┘ ┴
typ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘
494 have hx' : _ := exists_st_of_not_infinite hx, have hy' : _ := exists_st_of_not_infinite hy,
id └───────────────────────┘ └┘ └───────────────────────┘ └┘
src └───────────────────────┘ └───────────────────────┘
typ └───────────────────────┘ └┘ └───────────────────────┘ └┘
495 Exists.cases_on hx' $ Exists.cases_on hy' $ λ r hr s hs, not_infinite_of_exists_st $
id └─────────────┘ └─┘ └─────────────┘ └─┘ ┴ └┘ ┴ └┘ └───────────────────────┘
src └─────────────┘ └─────────────┘ └───────────────────────┘
typ └─────────────┘ └─┘ └─────────────┘ └─┘ ┴ └┘ ┴ └┘ └───────────────────────┘
496 ⟨s * r, is_st_mul hs hr⟩
id ┴ ┴ ┴ └───────┘ └┘ └┘
src ┴ └───────┘
typ ┴ ┴ ┴ └───────┘ └┘ └┘
497 ---
498
499 lemma st_add {x y : ℝ*} (hx : ¬infinite x) (hy : ¬infinite y) : st (x + y) = st x + st y :=
id └┘ ┴└──────┘ ┴ ┴└──────┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └┘ ┴└──────┘ ┴└──────┘ └┘ ┴ ┴ └┘ ┴ └┘
typ └┘ ┴└──────┘ ┴ ┴└──────┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └──────┘ └──────┘ └┘ └┘ └┘
500 have hx' : _ := is_st_st' hx,
id └───────┘ └┘
src └───────┘
typ └───────┘ └┘
501 have hy' : _ := is_st_st' hy,
id └───────┘ └┘
src └───────┘
typ └───────┘ └┘
502 have hxy : _ := is_st_st' (not_infinite_add hx hy),
id └───────┘ └──────────────┘ └┘ └┘
src └───────┘ └──────────────┘
typ └───────┘ └──────────────┘ └┘ └┘
503 have hxy' : _ := is_st_add hx' hy',
id └───────┘ └─┘ └─┘
src └───────┘
typ └───────┘ └─┘ └─┘
504 is_st_unique hxy hxy'
id └──────────┘ └─┘ └──┘
src └──────────┘
typ └──────────┘ └─┘ └──┘
505
506 lemma st_neg (x : ℝ*) : st (-x) = - st x :=
id └┘ └┘ ┴┴ ┴ ┴ └┘ ┴
src └┘ └┘ ┴ ┴ ┴ └┘
typ └┘ └┘ ┴┴ ┴ ┴ └┘ ┴
doc └┘ └┘ └┘
507 if h : infinite x
id └┘ └──────┘ ┴
src └┘ └──────┘
typ └┘ └──────┘ ┴
doc └──────┘
508 then by rw [st_infinite h, st_infinite (infinite_iff_infinite_neg.mp h), neg_zero]
id └─────────┘ ┴ └─────────┘ └──────────────────────────┘ ┴ └──────┘
src └──┘└─────────┘┴ └┘└─────────┘┴ └──────────────────────────┘┴ └─┘└──────┘└┘
typ └──┘└─────────┘┴┴└┘└─────────┘┴ └──────────────────────────┘┴┴└─┘└──────┘└┘
doc └──┘ ┴ └┘ ┴ ┴ └─┘ └┘
txt └──┘ ┴ └┘ ┴ ┴ └─┘ └┘
par └──┘ ┴ └┘ ┴ ┴ └─┘ └┘
pid └┘ ┴ └┘ ┴ ┴ └─┘ ┴┴
st └────────────────┘└────────────────────────────────────────────┘└────────┘┴┴
509 else is_st_unique (is_st_st' (not_infinite_neg h)) (is_st_neg (is_st_st' h))
id └──────────┘ └───────┘ └──────────────┘ ┴ └───────┘ └───────┘ ┴
src └──────────┘ └───────┘ └──────────────┘ └───────┘ └───────┘
typ └──────────┘ └───────┘ └──────────────┘ ┴ └───────┘ └───────┘ ┴
510
511 lemma st_mul {x y : ℝ*} (hx : ¬infinite x) (hy : ¬infinite y) : st (x * y) = (st x) * (st y) :=
id └┘ ┴└──────┘ ┴ ┴└──────┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └┘ ┴└──────┘ ┴└──────┘ └┘ ┴ ┴ └┘ ┴ └┘
typ └┘ ┴└──────┘ ┴ ┴└──────┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └──────┘ └──────┘ └┘ └┘ └┘
512 have hx' : _ := is_st_st' hx,
id └───────┘ └┘
src └───────┘
typ └───────┘ └┘
513 have hy' : _ := is_st_st' hy,
id └───────┘ └┘
src └───────┘
typ └───────┘ └┘
514 have hxy : _ := is_st_st' (not_infinite_mul hx hy),
id └───────┘ └──────────────┘ └┘ └┘
src └───────┘ └──────────────┘
typ └───────┘ └──────────────┘ └┘ └┘
515 have hxy' : _ := is_st_mul hx' hy',
id └───────┘ └─┘ └─┘
src └───────┘
typ └───────┘ └─┘ └─┘
516 is_st_unique hxy hxy'
id └──────────┘ └─┘ └──┘
src └──────────┘
typ └──────────┘ └─┘ └──┘
517
518 -- BASIC LEMMAS ABOUT INFINITESIMAL
519
520 theorem infinitesimal_def {x : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
521 infinitesimal x ↔ (∀ r : ℝ, r > 0 → -(r : ℝ*) < x ∧ x < r) :=
id └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
typ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────────┘ └┘
522 ⟨ λ hi r hr, by { convert (hi r hr), exact (zero_sub (of r)).symm, exact (zero_add (of r)).symm },
id └┘ ┴ └┘ └┘ ┴ └┘ └──────┘ └┘ ┴ └──────┘ └┘ ┴
src └──────┘ ┴ ┴ ┴ └────┘ └──────┘┴ └┘┴ └─────┘ └────┘ └──────┘┴ └┘┴ └──────┘
typ └┘ ┴ └┘ └──────┘ └┘┴┴┴└┘┴ └────┘ └──────┘┴ └┘┴┴└─────┘ └────┘ └──────┘┴ └┘┴┴└──────┘
doc └──────┘ ┴ ┴ ┴ └────┘ ┴ └┘┴ └─────┘ └────┘ ┴ └┘┴ └──────┘
txt └──────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─────┘ └────┘ ┴ ┴ └──────┘
par └──────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─────┘ └────┘ ┴ ┴ └──────┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘┴ ┴ ┴ ┴ └────┘└┘
st └──────────────────┘└────────────────────────────┘└─────────────────────────────┘└┘
523 λ hi d hd, by { convert (hi d hd), exact zero_sub (of d), exact zero_add (of d) } ⟩
id └┘ ┴ └┘ └┘ ┴ └┘ └──────┘ └┘ ┴ └──────┘ └┘ ┴
src └──────┘ ┴ ┴ ┴ └────┘└──────┘┴ └┘┴ ┴ └────┘└──────┘┴ └┘┴ └┘
typ └┘ ┴ └┘ └──────┘ └┘┴┴┴└┘┴ └────┘└──────┘┴ └┘┴┴┴ └────┘└──────┘┴ └┘┴┴└┘
doc └──────┘ ┴ ┴ ┴ └────┘ ┴ └┘┴ ┴ └────┘ ┴ └┘┴ └┘
txt └──────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └┘
par └──────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st └──────────────────┘└─────────────────────┘└──────────────────────┘└┘
524
525 theorem lt_of_pos_of_infinitesimal {x : ℝ*} : infinitesimal x → ∀ r : ℝ, r > 0 → x < r :=
id └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ └───────────┘ ┴ ┴ ┴
typ └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └───────────┘
526 λ hi r hr, ((infinitesimal_def.mp hi) r hr).2
id └┘ ┴ └┘ └───────────────┘└─┘ └┘ ┴ └┘ ┴
src └───────────────┘└─┘ ┴
typ └┘ ┴ └┘ └───────────────┘└─┘ └┘ ┴ └┘ ┴
527
528 theorem lt_neg_of_pos_of_infinitesimal {x : ℝ*} : infinitesimal x → ∀ r : ℝ, r > 0 → x > -r :=
id └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
src └┘ └───────────┘ ┴ ┴ ┴ ┴
typ └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └┘ └───────────┘
529 λ hi r hr, ((infinitesimal_def.mp hi) r hr).1
id └┘ ┴ └┘ └───────────────┘└─┘ └┘ ┴ └┘ ┴
src └───────────────┘└─┘ ┴
typ └┘ ┴ └┘ └───────────────┘└─┘ └┘ ┴ └┘ ┴
530
531 theorem gt_of_neg_of_infinitesimal {x : ℝ*} : infinitesimal x → ∀ r : ℝ, r < 0 → x > r :=
id └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ └───────────┘ ┴ ┴ ┴
typ └┘ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └───────────┘
532 λ hi r hr, by convert ((infinitesimal_def.mp hi) (-r) (neg_pos.mpr hr)).1;
id └┘ ┴ └┘ └──────────────────┘ └┘ ┴┴ └─────────┘ └┘
src └──────┘ └──────────────────┘┴ └┘ ┴ └┘ └─────────┘┴ └──┘
typ └┘ ┴ └┘ └──────┘ └──────────────────┘┴└┘└┘ ┴┴└┘ └─────────┘┴└┘└──┘
doc └──────┘ ┴ └┘ └┘ ┴ └──┘
txt └──────┘ ┴ └┘ └┘ ┴ └──┘
par └──────┘ ┴ └┘ └┘ ┴ └──┘
pid ┴ ┴ └┘ └┘ ┴ └┘└┘
st └─────────────────────────────────────────────────────────────
533 exact (neg_neg (of r)).symm
id └─────┘ └┘ ┴
src └────┘ └─────┘┴ └┘┴ └───────
typ └────┘ └─────┘┴ └┘┴┴└───────
doc └────┘ ┴ └┘┴ └───────
txt └────┘ ┴ ┴ └───────
par └────┘ ┴ ┴ └───────
pid ┴ ┴ ┴ └────┘└─
st ────────────────────────────
534
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
535 theorem abs_lt_real_iff_infinitesimal {x : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
536 infinitesimal x ↔ ∀ r : ℝ, r ≠ 0 → abs x < abs r :=
id └───────────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └───────────┘ ┴ ┴ ┴ └─┘ ┴ └─┘
typ └───────────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └───────────┘
537 ⟨ λ hi r hr, abs_lt.mpr (by rw [←of_eq_coe, ←of_abs U];
id └┘ ┴ └┘ └────┘└──┘ └───────┘ └────┘ ┴
src └────┘└──┘ └───┘└───────┘└─┘└────┘┴┴┴
typ └┘ ┴ └┘ └────┘└──┘ └───┘└───────┘└─┘└────┘┴┴┴
doc └───┘ └─┘ ┴ ┴
txt └───┘ └─┘ ┴ ┴
par └───┘ └─┘ ┴ ┴
pid └─┘ └─┘ ┴ ┴
st └─────────────┘└─────────┘┴└─
538 exact infinitesimal_def.mp hi (abs r) (abs_pos_of_ne_zero hr)),
id └──────────────────┘ └┘ └─┘ ┴ └────────────────┘ └┘
src └────┘└──────────────────┘┴ ┴ └─┘┴ └┘ └────────────────┘┴ ┴
typ └────┘└──────────────────┘┴└┘┴ └─┘┴┴└┘ └────────────────┘┴└┘┴
doc └────┘ ┴ ┴ ┴ └┘ ┴ ┴
txt └────┘ ┴ ┴ ┴ └┘ ┴ ┴
par └────┘ ┴ ┴ ┴ └┘ ┴ ┴
pid ┴ ┴ ┴ ┴ └┘ ┴ ┴
st ──────────────────────────────────────────────────────────────┘
539 λ hR, infinitesimal_def.mpr $ λ r hr, abs_lt.mp $
id └┘ └───────────────┘└──┘ ┴ └┘ └────┘└─┘
src └───────────────┘└──┘ └────┘└─┘
typ └┘ └───────────────┘└──┘ ┴ └┘ └────┘└─┘
540 (abs_of_pos $ of_lt_of_lt U hr : abs (r : ℝ*) = r) ▸ hR r $ ne_of_gt hr ⟩
id └────────┘ └─────────┘ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──────┘ └┘
src └────────┘ └─────────┘ ┴ └─┘ └┘ ┴ ┴ └──────┘
typ └────────┘ └─────────┘ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └──────┘ └┘
doc └┘
541
542 lemma infinitesimal_zero : infinitesimal 0 := is_st_refl_real 0
id └───────────┘ └─────────────┘
src └───────────┘ └─────────────┘
typ └───────────┘ └─────────────┘
doc └───────────┘
543
544 lemma zero_of_infinitesimal_real {r : ℝ} : infinitesimal r → r = 0 := eq_of_is_st_real
id ┴ └───────────┘ ┴ ┴ ┴ └──────────────┘
src ┴ └───────────┘ ┴ └──────────────┘
typ ┴ └───────────┘ ┴ ┴ ┴ └──────────────┘
doc └───────────┘
545
546 lemma zero_iff_infinitesimal_real {r : ℝ} : infinitesimal r ↔ r = 0 :=
id ┴ └───────────┘ ┴ ┴ ┴ ┴
src ┴ └───────────┘ ┴ ┴
typ ┴ └───────────┘ ┴ ┴ ┴ ┴
doc └───────────┘
547 ⟨zero_of_infinitesimal_real, λ hr, by rw hr; exact infinitesimal_zero⟩
id └────────────────────────┘ └┘ └┘ └────────────────┘
src └────────────────────────┘ └─┘ └────┘└────────────────┘
typ └────────────────────────┘ └┘ └─┘└┘ └────┘└────────────────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └──────────────────────────────┘
548
549 lemma infinitesimal_add {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
550 infinitesimal x → infinitesimal y → infinitesimal (x + y) :=
id └───────────┘ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
src └───────────┘ └───────────┘ └───────────┘ ┴
typ └───────────┘ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘ └───────────┘ └───────────┘
551 zero_add 0 ▸ is_st_add
id └──────┘ ┴ └───────┘
src └──────┘ ┴ └───────┘
typ └──────┘ ┴ └───────┘
552
553 lemma infinitesimal_neg {x : ℝ*} : infinitesimal x → infinitesimal (-x) :=
id └┘ └───────────┘ ┴ └───────────┘ ┴┴
src └┘ └───────────┘ └───────────┘ ┴
typ └┘ └───────────┘ ┴ └───────────┘ ┴┴
doc └┘ └───────────┘ └───────────┘
554 (neg_zero : -(0 : ℝ) = 0) ▸ is_st_neg
id └──────┘ ┴ ┴ ┴ ┴ └───────┘
src └──────┘ ┴ ┴ ┴ ┴ └───────┘
typ └──────┘ ┴ ┴ ┴ ┴ └───────┘
555
556 lemma infinitesimal_neg_iff {x : ℝ*} : infinitesimal x ↔ infinitesimal (-x) :=
id └┘ └───────────┘ ┴ ┴ └───────────┘ ┴┴
src └┘ └───────────┘ ┴ └───────────┘ ┴
typ └┘ └───────────┘ ┴ ┴ └───────────┘ ┴┴
doc └┘ └───────────┘ └───────────┘
557 ⟨infinitesimal_neg, λ h, (neg_neg x) ▸ @infinitesimal_neg (-x) h⟩
id └───────────────┘ ┴ └─────┘ ┴ ┴ └───────────────┘ ┴┴ ┴
src └───────────────┘ └─────┘ ┴ └───────────────┘ ┴
typ └───────────────┘ ┴ └─────┘ ┴ ┴ └───────────────┘ ┴┴ ┴
558
559 lemma infinitesimal_mul {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
560 infinitesimal x → infinitesimal y → infinitesimal (x * y) :=
id └───────────┘ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
src └───────────┘ └───────────┘ └───────────┘ ┴
typ └───────────┘ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘ └───────────┘ └───────────┘
561 zero_mul 0 ▸ is_st_mul
id └──────┘ ┴ └───────┘
src └──────┘ ┴ └───────┘
typ └──────┘ ┴ └───────┘
562
563 theorem infinitesimal_of_tendsto_zero {f : ℕ → ℝ} :
id ┴ ┴
src ┴ ┴
typ ┴ ┴
564 tendsto f at_top (𝓝 0) → infinitesimal (of_seq f) :=
id └─────┘ ┴ └────┘ ┴ └───────────┘ └────┘ ┴
src └─────┘ └────┘ ┴ └───────────┘ └────┘
typ └─────┘ ┴ └────┘ ┴ └───────────┘ └────┘ ┴
doc └─────┘ └────┘ ┴ └───────────┘
565 λ hf d hd, by rw [←of_eq_coe, ←of_eq_coe, sub_eq_add_neg,
id └┘ ┴ └┘ └───────┘ └───────┘ └────────────┘
src └───┘└───────┘└─┘└───────┘└┘└────────────┘└─
typ └┘ ┴ └┘ └───┘└───────┘└─┘└───────┘└┘└────────────┘└─
doc └───┘ └─┘ └┘ └─
txt └───┘ └─┘ └┘ └─
par └───┘ └─┘ └┘ └─
pid └─┘ └─┘ └┘ └─
st └─────────────┘└──────────┘└──────────────┘└─
566 ←of_neg, ←of_add, ←of_add, zero_add, zero_add, of_eq_coe, of_eq_coe];
id └────┘ └────┘ └────┘ └──────┘ └──────┘ └───────┘ └───────┘
src ──┘└────┘└─┘└────┘└─┘└────┘└┘└──────┘└┘└──────┘└┘└───────┘└┘└───────┘┴
typ ──┘└────┘└─┘└────┘└─┘└────┘└┘└──────┘└┘└──────┘└┘└───────┘└┘└───────┘┴
doc ──┘ └─┘ └─┘ └┘ └┘ └┘ └┘ ┴
txt ──┘ └─┘ └─┘ └┘ └┘ └┘ └┘ ┴
par ──┘ └─┘ └─┘ └┘ └┘ └┘ └┘ ┴
pid ──┘ └─┘ └─┘ └┘ └┘ └┘ └┘ ┴
st ────────┘└───────┘└───────┘└────────┘└────────┘└─────────┘└─────────┘┴└─
567 exact ⟨neg_lt_of_tendsto_zero_of_pos hf hd, lt_of_tendsto_zero_of_pos hf hd⟩
id └───────────────────────────┘ └───────────────────────┘ └┘ └┘
src └────┘ └───────────────────────────┘┴ ┴ └┘└───────────────────────┘┴ ┴ └─
typ └────┘ └───────────────────────────┘┴ ┴ └┘└───────────────────────┘┴└┘┴└┘└─
doc └────┘ ┴ ┴ └┘ ┴ ┴ └─
txt └────┘ ┴ ┴ └┘ ┴ ┴ └─
par └────┘ ┴ ┴ └┘ ┴ ┴ └─
pid ┴ ┴ ┴ └┘ ┴ ┴ ┴└
st ─────────────────────────────────────────────────────────────────────────────
568
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
569 theorem infinitesimal_epsilon : infinitesimal ε :=
id └───────────┘ ┴
src └───────────┘ ┴
typ └───────────┘ ┴
doc └───────────┘ ┴
570 infinitesimal_of_tendsto_zero tendsto_inverse_at_top_nhds_0_nat
id └───────────────────────────┘ └───────────────────────────────┘
src └───────────────────────────┘ └───────────────────────────────┘
typ └───────────────────────────┘ └───────────────────────────────┘
571
572 lemma not_real_of_infinitesimal_ne_zero (x : ℝ*) :
id └┘
src └┘
typ └┘
doc └┘
573 infinitesimal x → x ≠ 0 → ∀ r : ℝ, x ≠ of r :=
id └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src └───────────┘ ┴ ┴ ┴ └┘
typ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └───────────┘ └┘
574 λ hi hx r hr, hx (is_st_unique (hr.symm ▸ is_st_refl_real r : is_st x r) hi ▸ hr : x = of 0)
id └┘ └┘ ┴ └┘ └┘ └──────────┘ └┘└───┘ ┴ └─────────────┘ ┴ └───┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘
src └──────────┘ └───┘ ┴ └─────────────┘ └───┘ ┴ ┴ └┘
typ └┘ └┘ ┴ └┘ └┘ └──────────┘ └┘└───┘ ┴ └─────────────┘ ┴ └───┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘
doc └───┘ └┘
575
576 theorem infinitesimal_sub_is_st {x : ℝ*} {r : ℝ} (hxr : is_st x r) : infinitesimal (x - r) :=
id └┘ ┴ └───┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └┘ ┴ └───┘ └───────────┘ ┴
typ └┘ ┴ └───┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └┘ └───┘ └───────────┘
577 show is_st (x + -r) 0, by rw ←add_neg_self r; exact is_st_add hxr (is_st_refl_real (-r))
id └───┘ ┴ ┴ ┴┴ └──────────┘ ┴ └───────┘ └─┘ └─────────────┘ ┴┴
src └───┘ ┴ ┴ └──┘└──────────┘┴ └────┘└───────┘┴ ┴ └─────────────┘┴ ┴ └──
typ └───┘ ┴ ┴ ┴┴ └──┘└──────────┘┴┴ └────┘└───────┘┴└─┘┴ └─────────────┘┴ ┴┴└──
doc └───┘ └──┘ ┴ └────┘ ┴ ┴ ┴ └──
txt └──┘ ┴ └────┘ ┴ ┴ ┴ └──
par └──┘ ┴ └────┘ ┴ ┴ ┴ └──
pid └┘ ┴ ┴ ┴ ┴ ┴ └┘└
st └───────────────────────────────────────────────────────────────
578
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
579 theorem infinitesimal_sub_st {x : ℝ*} (hx : ¬infinite x) : infinitesimal (x - st x) :=
id └┘ ┴└──────┘ ┴ └───────────┘ ┴ ┴ └┘ ┴
src └┘ ┴└──────┘ └───────────┘ ┴ └┘
typ └┘ ┴└──────┘ ┴ └───────────┘ ┴ ┴ └┘ ┴
doc └┘ └──────┘ └───────────┘ └┘
580 infinitesimal_sub_is_st $ is_st_st' hx
id └─────────────────────┘ └───────┘ └┘
src └─────────────────────┘ └───────┘
typ └─────────────────────┘ └───────┘ └┘
581
582 lemma infinite_pos_iff_infinitesimal_inv_pos {x : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
583 infinite_pos x ↔ (infinitesimal x⁻¹ ∧ x⁻¹ > 0) :=
id └──────────┘ ┴ ┴ └───────────┘ ┴└┘ ┴ ┴└┘ ┴
src └──────────┘ ┴ └───────────┘ └┘ ┴ └┘ ┴
typ └──────────┘ ┴ ┴ └───────────┘ ┴└┘ ┴ ┴└┘ ┴
doc └──────────┘ └───────────┘
584 ⟨ λ hip, ⟨ infinitesimal_def.mpr $ λ r hr,
id └─┘ └───────────────┘└──┘ ┴ └┘
src └───────────────┘└──┘
typ └─┘ └───────────────┘└──┘ ┴ └┘
585 ⟨ lt_trans (of_lt_of_lt U (neg_neg_of_pos hr)) (inv_pos (hip 0)),
id └──────┘ └─────────┘ ┴ └────────────┘ └┘ └─────┘ └─┘
src └──────┘ └─────────┘ ┴ └────────────┘ └─────┘
typ └──────┘ └─────────┘ ┴ └────────────┘ └┘ └─────┘ └─┘
586 (inv_lt (of_lt_of_lt U hr) (hip 0)).mp (by convert hip r⁻¹) ⟩,
id └────┘ └─────────┘ ┴ └┘ └─┘ └┘ └─┘ ┴└┘
src └────┘ └─────────┘ ┴ └┘ └──────┘ ┴ └┘
typ └────┘ └─────────┘ ┴ └┘ └─┘ └┘ └──────┘└─┘┴┴└┘
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴ ┴
st └──────────────┘
587 inv_pos $ hip 0 ⟩,
id └─────┘ └─┘
src └─────┘
typ └─────┘ └─┘
588 λ ⟨hi, hp⟩ r, @classical.by_cases (r = 0) (x > (r : ℝ*)) (λ h, eq.substr h (inv_pos'.mp hp)) $
id ┴└┘ └┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────┘ ┴ └──────┘└─┘
src └────────────────┘ ┴ ┴ └┘ └───────┘ └──────┘└─┘
typ ┴└┘ └┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───────┘ ┴ └──────┘└─┘
doc └┘
589 λ h, lt_of_le_of_lt (of_le_of_le (le_abs_self r))
id ┴ └────────────┘ └─────────┘ └─────────┘ ┴
src └────────────┘ └─────────┘ └─────────┘
typ ┴ └────────────┘ └─────────┘ └─────────┘ ┴
st ┴
590 ((inv_lt_inv (inv_pos'.mp hp) (of_lt_of_lt U (abs_pos_of_ne_zero h))).mp
id └────────┘ └──────┘└─┘ └─────────┘ ┴ └────────────────┘ ┴ └┘
src └────────┘ └──────┘└─┘ └─────────┘ ┴ └────────────────┘ └┘
typ └────────┘ └──────┘└─┘ └─────────┘ ┴ └────────────────┘ ┴ └┘
591 ((infinitesimal_def.mp hi) ((abs r)⁻¹) (inv_pos (abs_pos_of_ne_zero h))).2) ⟩
id └───────────────┘└─┘ └─┘ ┴ └┘ └─────┘ └────────────────┘ ┴ ┴
src └───────────────┘└─┘ └─┘ └┘ └─────┘ └────────────────┘ ┴
typ └───────────────┘└─┘ └─┘ ┴ └┘ └─────┘ └────────────────┘ ┴ ┴
592
593 lemma infinite_neg_iff_infinitesimal_inv_neg {x : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
594 infinite_neg x ↔ (infinitesimal x⁻¹ ∧ x⁻¹ < 0) :=
id └──────────┘ ┴ ┴ └───────────┘ ┴└┘ ┴ ┴└┘ ┴
src └──────────┘ ┴ └───────────┘ └┘ ┴ └┘ ┴
typ └──────────┘ ┴ ┴ └───────────┘ ┴└┘ ┴ ┴└┘ ┴
doc └──────────┘ └───────────┘
595 ⟨ λ hin, have hin' : _ := infinite_pos_iff_infinitesimal_inv_pos.mp
id └─┘ └────────────────────────────────────┘└─┘
src └────────────────────────────────────┘└─┘
typ └─┘ └────────────────────────────────────┘└─┘
596 (infinite_pos_neg_of_infinite_neg hin),
id └──────────────────────────────┘ └─┘
src └──────────────────────────────┘
typ └──────────────────────────────┘ └─┘
597 by rwa [infinitesimal_neg_iff, ←neg_pos,
id └───────────────────┘ └─────┘
src └───┘└───────────────────┘└─┘└─────┘└─
typ └───┘└───────────────────┘└─┘└─────┘└─
doc └───┘ └─┘ └─
txt └───┘ └─┘ └─
par └───┘ └─┘ └─
pid └┘ └─┘ └─
st └─────────────────────────┘└────────┘└─
598 neg_inv (λ h0, lt_irrefl x (by convert hin 0) : x ≠ 0)],
id └─────┘ └───────┘ ┴ └─┘ ┴
src ───┘└─────┘┴ └───┘└───────┘┴ ┴ ┴└──────┘ └┘└──┘ ┴┴└──┘
typ ───┘└─────┘┴ └───┘└───────┘┴┴┴ ┴└──────┘└─┘└┘└──┘ ┴┴└──┘
doc ───┘ ┴ └───┘ ┴ ┴ ┴└──────┘ └┘└──┘ ┴ └──┘
txt ───┘ ┴ └───┘ ┴ ┴ ┴└──────┘ └┘└──┘ ┴ └──┘
par ───┘ ┴ └───┘ ┴ ┴ ┴└──────┘ └┘└──┘ ┴ └──┘
pid ───┘ ┴ └───┘ ┴ ┴ └───────┘ └────┘ ┴ └──┘
st ─────────────────────────────────┘└────────────┘└────────┘┴
599 λ hin, have h0 : x ≠ 0 := λ h0, (lt_irrefl (0 : ℝ*) (by convert hin.2; rw [h0, inv_zero])),
id └─┘ ┴ ┴ └┘ └───────┘ └┘ └─┘ └┘ └──────┘
src ┴ └───────┘ └┘ └──────┘ └┘ └──┘ └┘└──────┘┴
typ └─┘ ┴ ┴ └┘ └───────┘ └┘ └──────┘└─┘└┘ └──┘└┘└┘└──────┘┴
doc └┘ └──────┘ └┘ └──┘ └┘ ┴
txt └──────┘ └┘ └──┘ └┘ ┴
par └──────┘ └┘ └──┘ └┘ ┴
pid ┴ └┘ └┘ └┘ ┴
st └──────────────────┘└┘└────────┘┴
600 by rwa [←neg_pos, infinitesimal_neg_iff, neg_inv h0,
id └─────┘ └───────────────────┘ └─────┘ └┘
src └────┘└─────┘└┘└───────────────────┘└┘└─────┘┴ └─
typ └────┘└─────┘└┘└───────────────────┘└┘└─────┘┴└┘└─
doc └────┘ └┘ └┘ ┴ └─
txt └────┘ └┘ └┘ ┴ └─
par └────┘ └┘ └┘ ┴ └─
pid └─┘ └┘ └┘ ┴ └─
st └────────────┘└─────────────────────┘└──────────┘└─
601 ←infinite_pos_iff_infinitesimal_inv_pos, ←infinite_neg_iff_infinite_pos_neg] at hin ⟩
id └────────────────────────────────────┘ └───────────────────────────────┘
src ────┘└────────────────────────────────────┘└─┘└───────────────────────────────┘└───────┘
typ ────┘└────────────────────────────────────┘└─┘└───────────────────────────────┘└───────┘
doc ────┘ └─┘ └───────┘
txt ────┘ └─┘ └───────┘
par ────┘ └─┘ └───────┘
pid ────┘ └─┘ ┴└─────┘┴
st ──────────────────────────────────────────┘└──────────────────────────────────┘┴└──────┘
602
603 theorem infinitesimal_inv_of_infinite {x : ℝ*} : infinite x → infinitesimal x⁻¹ :=
id └┘ └──────┘ ┴ └───────────┘ ┴└┘
src └┘ └──────┘ └───────────┘ └┘
typ └┘ └──────┘ ┴ └───────────┘ ┴└┘
doc └┘ └──────┘ └───────────┘
604 λ hi, or.cases_on hi
id └┘ └─────────┘ └┘
src └─────────┘
typ └┘ └─────────┘ └┘
605 (λ hip, (infinite_pos_iff_infinitesimal_inv_pos.mp hip).1)
id └─┘ └────────────────────────────────────┘└─┘ └─┘ ┴
src └────────────────────────────────────┘└─┘ ┴
typ └─┘ └────────────────────────────────────┘└─┘ └─┘ ┴
606 (λ hin, (infinite_neg_iff_infinitesimal_inv_neg.mp hin).1)
id └─┘ └────────────────────────────────────┘└─┘ └─┘ ┴
src └────────────────────────────────────┘└─┘ ┴
typ └─┘ └────────────────────────────────────┘└─┘ └─┘ ┴
607
608 theorem infinite_of_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) (hi : infinitesimal x⁻¹ ) :
id └┘ ┴ ┴ └───────────┘ ┴└┘
src └┘ ┴ └───────────┘ └┘
typ └┘ ┴ ┴ └───────────┘ ┴└┘
doc └┘ └───────────┘
609 infinite x :=
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
610 begin
st └─────
611 cases (lt_or_gt_of_ne h0) with hn hp,
id └────────────┘ └┘
src └────┘ └────────────┘┴ └──────────┘
typ └────┘ └────────────┘┴└┘└──────────┘
doc └────┘ ┴ └──────────┘
txt └────┘ ┴ └──────────┘
par └────┘ ┴ └──────────┘
pid ┴ ┴ ┴└─────────┘
st ─────────────────────────────────────┘└─
612 { exact or.inr (infinite_neg_iff_infinitesimal_inv_neg.mpr ⟨hi, inv_neg'.mpr hn⟩) },
id └────┘ └────────────────────────────────────────┘ └┘ └──────────┘ └┘
src └────┘└────┘┴ └────────────────────────────────────────┘┴ └┘└──────────┘┴ └─┘
typ └────┘└────┘┴ └────────────────────────────────────────┘┴ └┘└┘└──────────┘┴└┘└─┘
doc └────┘ ┴ ┴ └┘ ┴ └─┘
txt └────┘ ┴ ┴ └┘ ┴ └─┘
par └────┘ ┴ ┴ └┘ ┴ └─┘
pid ┴ ┴ ┴ └┘ ┴ └┘┴
st ───┘└──────────────────────────────────────────────────────────────────────────────┘└┘└
613 { exact or.inl (infinite_pos_iff_infinitesimal_inv_pos.mpr ⟨hi, inv_pos'.mpr hp⟩) }
id └────┘ └────────────────────────────────────────┘ └┘ └──────────┘ └┘
src └────┘└────┘┴ └────────────────────────────────────────┘┴ └┘└──────────┘┴ └─┘
typ └────┘└────┘┴ └────────────────────────────────────────┘┴ └┘└┘└──────────┘┴└┘└─┘
doc └────┘ ┴ ┴ └┘ ┴ └─┘
txt └────┘ ┴ ┴ └┘ ┴ └─┘
par └────┘ ┴ ┴ └┘ ┴ └─┘
pid ┴ ┴ ┴ └┘ ┴ └┘┴
st ───────────────────────────────────────────────────────────────────────────────────┘└─
614 end
st ──┘
615
616 theorem infinite_iff_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) : infinite x ↔ infinitesimal x⁻¹ :=
id └┘ ┴ ┴ └──────┘ ┴ ┴ └───────────┘ ┴└┘
src └┘ ┴ └──────┘ ┴ └───────────┘ └┘
typ └┘ ┴ ┴ └──────┘ ┴ ┴ └───────────┘ ┴└┘
doc └┘ └──────┘ └───────────┘
617 ⟨ infinitesimal_inv_of_infinite, infinite_of_infinitesimal_inv h0 ⟩
id └───────────────────────────┘ └───────────────────────────┘ └┘
src └───────────────────────────┘ └───────────────────────────┘
typ └───────────────────────────┘ └───────────────────────────┘ └┘
618
619 lemma infinitesimal_pos_iff_infinite_pos_inv {x : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
620 infinite_pos x⁻¹ ↔ (infinitesimal x ∧ x > 0) :=
id └──────────┘ ┴└┘ ┴ └───────────┘ ┴ ┴ ┴ ┴
src └──────────┘ └┘ ┴ └───────────┘ ┴ ┴
typ └──────────┘ ┴└┘ ┴ └───────────┘ ┴ ┴ ┴ ┴
doc └──────────┘ └───────────┘
621 by convert infinite_pos_iff_infinitesimal_inv_pos; simp only [inv_inv']
id └────────────────────────────────────┘ └──────┘
src └──────┘└────────────────────────────────────┘ └─────────┘└──────┘└─
typ └──────┘└────────────────────────────────────┘ └─────────┘└──────┘└─
doc └──────┘ └─────────┘ └─
txt └──────┘ └─────────┘ └─
par └──────┘ └─────────┘ └─
pid ┴ ┴└──┘└┘ ┴└
st └─────────────────────────────────────────────────────────────────────
622
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
623 lemma infinitesimal_neg_iff_infinite_neg_inv {x : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
624 infinite_neg x⁻¹ ↔ (infinitesimal x ∧ x < 0) :=
id └──────────┘ ┴└┘ ┴ └───────────┘ ┴ ┴ ┴ ┴
src └──────────┘ └┘ ┴ └───────────┘ ┴ ┴
typ └──────────┘ ┴└┘ ┴ └───────────┘ ┴ ┴ ┴ ┴
doc └──────────┘ └───────────┘
625 by convert infinite_neg_iff_infinitesimal_inv_neg; simp only [inv_inv']
id └────────────────────────────────────┘ └──────┘
src └──────┘└────────────────────────────────────┘ └─────────┘└──────┘└─
typ └──────┘└────────────────────────────────────┘ └─────────┘└──────┘└─
doc └──────┘ └─────────┘ └─
txt └──────┘ └─────────┘ └─
par └──────┘ └─────────┘ └─
pid ┴ ┴└──┘└┘ ┴└
st └─────────────────────────────────────────────────────────────────────
626
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
627 theorem infinitesimal_iff_infinite_inv {x : ℝ*} (h : x ≠ 0) : infinitesimal x ↔ infinite x⁻¹ :=
id └┘ ┴ ┴ └───────────┘ ┴ ┴ └──────┘ ┴└┘
src └┘ ┴ └───────────┘ ┴ └──────┘ └┘
typ └┘ ┴ ┴ └───────────┘ ┴ ┴ └──────┘ ┴└┘
doc └┘ └───────────┘ └──────┘
628 by convert (infinite_iff_infinitesimal_inv (inv_ne_zero h)).symm; simp only [inv_inv']
id └────────────────────────────┘ └─────────┘ ┴ └──────┘
src └──────┘ └────────────────────────────┘┴ └─────────┘┴ └─────┘ └─────────┘└──────┘└─
typ └──────┘ └────────────────────────────┘┴ └─────────┘┴┴└─────┘ └─────────┘└──────┘└─
doc └──────┘ ┴ ┴ └─────┘ └─────────┘ └─
txt └──────┘ ┴ ┴ └─────┘ └─────────┘ └─
par └──────┘ ┴ ┴ └─────┘ └─────────┘ └─
pid ┴ ┴ ┴ └────┘┴ ┴└──┘└┘ ┴└
st └────────────────────────────────────────────────────────────────────────────────────
629
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
630 -- ST STUFF THAT REQUIRES INFINITESIMAL MACHINERY
src ──────────────────────────────────────────────────
typ ──────────────────────────────────────────────────
doc ──────────────────────────────────────────────────
txt ──────────────────────────────────────────────────
par ──────────────────────────────────────────────────
pid ──────────────────────────────────────────────────
st ──────────────────────────────────────────────────
631
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
632 theorem is_st_of_tendsto {f : ℕ → ℝ} {r : ℝ} (hf : tendsto f at_top (𝓝 r)) :
id ┴ ┴ ┴ └─────┘ ┴ └────┘ ┴ ┴
src ┴ ┴ ┴ └─────┘ └────┘ ┴
typ ┴ ┴ ┴ └─────┘ ┴ └────┘ ┴ ┴
doc └─────┘ └────┘ ┴
633 is_st (of_seq f) r :=
id └───┘ └────┘ ┴ ┴
src └───┘ └────┘
typ └───┘ └────┘ ┴ ┴
doc └───┘
634 have hg : tendsto (λ n, f n - r) at_top (𝓝 0) :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
src └─────┘ ┴ └────┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
doc └─────┘ └────┘ ┴
635 (sub_self r) ▸ (hf.sub tendsto_const_nhds),
id └──────┘ ┴ ┴ └┘└──┘ └────────────────┘
src └──────┘ ┴ └──┘ └────────────────┘
typ └──────┘ ┴ ┴ └┘└──┘ └────────────────┘
636 by rw [←(zero_add r), ←(sub_add_cancel f (λ n, r))];
id └──────┘ ┴ └────────────┘ ┴ ┴
src └───┘ └──────┘┴ └──┘ └────────────┘┴ ┴ └──┘ └─┘
typ └───┘ └──────┘┴┴└──┘ └────────────┘┴┴┴ └──┘┴└─┘
doc └───┘ ┴ └──┘ ┴ ┴ └──┘ └─┘
txt └───┘ ┴ └──┘ ┴ ┴ └──┘ └─┘
par └───┘ ┴ └──┘ ┴ ┴ └──┘ └─┘
pid └─┘ ┴ └──┘ ┴ ┴ └──┘ └─┘
st └────────────────┘└────────────────────────────┘┴└─
637 exact is_st_add (infinitesimal_of_tendsto_zero hg) (is_st_refl_real r)
id └───────┘ └───────────────────────────┘ └┘ └─────────────┘ ┴
src └────┘└───────┘┴ └───────────────────────────┘┴ └┘ └─────────────┘┴ └─
typ └────┘└───────┘┴ └───────────────────────────┘┴└┘└┘ └─────────────┘┴┴└─
doc └────┘ ┴ ┴ └┘ ┴ └─
txt └────┘ ┴ ┴ └┘ ┴ └─
par └────┘ ┴ ┴ └┘ ┴ └─
pid ┴ ┴ ┴ └┘ ┴ ┴└
st ───────────────────────────────────────────────────────────────────────
638
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
639 lemma is_st_inv {x : ℝ*} {r : ℝ} (hi : ¬ infinitesimal x) : is_st x r → is_st x⁻¹ r⁻¹ :=
id └┘ ┴ ┴ └───────────┘ ┴ └───┘ ┴ ┴ └───┘ ┴└┘ ┴└┘
src └┘ ┴ ┴ └───────────┘ └───┘ └───┘ └┘ └┘
typ └┘ ┴ ┴ └───────────┘ ┴ └───┘ ┴ ┴ └───┘ ┴└┘ ┴└┘
doc └┘ └───────────┘ └───┘ └───┘
640 λ hxr, have h : x ≠ 0 := (λ h, hi (h.symm ▸ infinitesimal_zero)),
id └─┘ ┴ ┴ ┴ └┘ ┴└───┘ ┴ └────────────────┘
src ┴ └───┘ ┴ └────────────────┘
typ └─┘ ┴ ┴ ┴ └┘ ┴└───┘ ┴ └────────────────┘
641 have H : _ := exists_st_of_not_infinite $ not_imp_not.mpr (infinitesimal_iff_infinite_inv h).mpr hi,
id └───────────────────────┘ └─────────┘└──┘ └────────────────────────────┘ ┴ └─┘ └┘
src └───────────────────────┘ └─────────┘└──┘ └────────────────────────────┘ └─┘
typ └───────────────────────┘ └─────────┘└──┘ └────────────────────────────┘ ┴ └─┘ └┘
642 Exists.cases_on H $ λ s hs,
id └─────────────┘ ┴ ┴ └┘
src └─────────────┘
typ └─────────────┘ ┴ ┴ └┘
643 have H' : is_st 1 (r * s) := mul_inv_cancel h ▸ is_st_mul hxr hs,
id └───┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ └───────┘ └─┘ └┘
src └───┘ ┴ └────────────┘ ┴ └───────┘
typ └───┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ └───────┘ └─┘ └┘
doc └───┘
644 have H'' : s = r⁻¹ := one_div_eq_inv r ▸ eq_one_div_of_mul_eq_one (eq_of_is_st_real H').symm,
id ┴ ┴ ┴└┘ └────────────┘ ┴ ┴ └──────────────────────┘ └──────────────┘ └┘ └──┘
src ┴ └┘ └────────────┘ ┴ └──────────────────────┘ └──────────────┘ └──┘
typ ┴ ┴ ┴└┘ └────────────┘ ┴ ┴ └──────────────────────┘ └──────────────┘ └┘ └──┘
645 H'' ▸ hs
id └─┘ ┴ └┘
src ┴
typ └─┘ ┴ └┘
646
647 lemma st_inv (x : ℝ*) : st x⁻¹ = (st x)⁻¹ :=
id └┘ └┘ ┴└┘ ┴ └┘ ┴ └┘
src └┘ └┘ └┘ ┴ └┘ └┘
typ └┘ └┘ ┴└┘ ┴ └┘ ┴ └┘
doc └┘ └┘ └┘
648 begin
st └─────
649 by_cases h0 : x = 0,
id ┴ ┴
src └───────┘ └─┘ ┴┴└┘
typ └───────┘ └─┘┴┴┴└┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ────────────────────┘└─
650 rw [h0, inv_zero, ←of_zero, of_eq_coe, st_id_real, inv_zero],
id └┘ └──────┘ └─────┘ └───────┘ └────────┘ └──────┘
src └──┘ └┘└──────┘└─┘└─────┘└┘└───────┘└┘└────────┘└┘└──────┘┴
typ └──┘└┘└┘└──────┘└─┘└─────┘└┘└───────┘└┘└────────┘└┘└──────┘┴
doc └──┘ └┘ └─┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └─┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └─┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └─┘ └┘ └┘ └┘ ┴
st ───────┘└────────┘└────────┘└─────────┘└──────────┘└────────┘└──
651 by_cases h1 : infinitesimal x,
id └───────────┘ ┴
src └───────┘ └─┘└───────────┘┴
typ └───────┘ └─┘└───────────┘┴┴
doc └───────┘ └─┘└───────────┘┴
txt └───────┘ └─┘ ┴
par └───────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ──────────────────────────────┘└─
652 rw [st_infinite ((infinitesimal_iff_infinite_inv h0).mp h1), st_of_is_st h1, inv_zero],
id └─────────┘ └────────────────────────────┘ └┘ └┘ └─────────┘ └┘ └──────┘
src └──┘└─────────┘┴ └────────────────────────────┘┴ └───┘ └─┘└─────────┘┴ └┘└──────┘┴
typ └──┘└─────────┘┴ └────────────────────────────┘┴└┘└───┘└┘└─┘└─────────┘┴└┘└┘└──────┘┴
doc └──┘ ┴ ┴ └───┘ └─┘ ┴ └┘ ┴
txt └──┘ ┴ ┴ └───┘ └─┘ ┴ └┘ ┴
par └──┘ ┴ ┴ └───┘ └─┘ ┴ └┘ ┴
pid └┘ ┴ ┴ └───┘ └─┘ ┴ └┘ ┴
st ────────────────────────────────────────────────────────────┘└──────────────┘└────────┘└──
653 by_cases h2 : infinite x,
id └──────┘ ┴
src └───────┘ └─┘└──────┘┴
typ └───────┘ └─┘└──────┘┴┴
doc └───────┘ └─┘└──────┘┴
txt └───────┘ └─┘ ┴
par └───────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────────────────────────┘└─
654 rw [st_of_is_st (infinitesimal_inv_of_infinite h2), st_infinite h2, inv_zero],
id └─────────┘ └───────────────────────────┘ └┘ └─────────┘ └┘ └──────┘
src └──┘└─────────┘┴ └───────────────────────────┘┴ └─┘└─────────┘┴ └┘└──────┘┴
typ └──┘└─────────┘┴ └───────────────────────────┘┴└┘└─┘└─────────┘┴└┘└┘└──────┘┴
doc └──┘ ┴ ┴ └─┘ ┴ └┘ ┴
txt └──┘ ┴ ┴ └─┘ ┴ └┘ ┴
par └──┘ ┴ ┴ └─┘ ┴ └┘ ┴
pid └┘ ┴ ┴ └─┘ ┴ └┘ ┴
st ───────────────────────────────────────────────────┘└──────────────┘└────────┘└──
655 exact st_of_is_st (is_st_inv h1 (is_st_st' h2)),
id └─────────┘ └───────┘ └┘ └───────┘ └┘
src └────┘└─────────┘┴ └───────┘┴ ┴ └───────┘┴ └┘
typ └────┘└─────────┘┴ └───────┘┴└┘┴ └───────┘┴└┘└┘
doc └────┘ ┴ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ └┘
st ────────────────────────────────────────────────┘└─
656 end
st ──┘
657
658 -- INFINITE STUFF THAT REQUIRES INFINITESIMAL MACHINERY
659
660 lemma infinite_pos_omega : infinite_pos ω :=
id └──────────┘ ┴
src └──────────┘ ┴
typ └──────────┘ ┴
doc └──────────┘ ┴
661 infinite_pos_iff_infinitesimal_inv_pos.mpr ⟨infinitesimal_epsilon, epsilon_pos⟩
id └────────────────────────────────────┘└──┘ └───────────────────┘ └─────────┘
src └────────────────────────────────────┘└──┘ └───────────────────┘ └─────────┘
typ └────────────────────────────────────┘└──┘ └───────────────────┘ └─────────┘
662
663 lemma infinite_omega : infinite ω :=
id └──────┘ ┴
src └──────┘ ┴
typ └──────┘ ┴
doc └──────┘ ┴
664 (infinite_iff_infinitesimal_inv omega_ne_zero).mpr infinitesimal_epsilon
id └────────────────────────────┘ └───────────┘ └─┘ └───────────────────┘
src └────────────────────────────┘ └───────────┘ └─┘ └───────────────────┘
typ └────────────────────────────┘ └───────────┘ └─┘ └───────────────────┘
665
666 lemma infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
667 infinite_pos x → ¬ infinitesimal y → y > 0 → infinite_pos (x * y) :=
id └──────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴ └───────────┘ ┴ └──────────┘ ┴
typ └──────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └───────────┘ └──────────┘
668 λ hx hy₁ hy₂ r, have hy₁' : _ := not_forall.mp (by rw infinitesimal_def at hy₁; exact hy₁),
id └┘ └─┘ └─┘ ┴ └────────┘└─┘ └───────────────┘ └─┘
src └────────┘└─┘ └─┘└───────────────┘└─────┘ └────┘
typ └┘ └─┘ └─┘ ┴ └────────┘└─┘ └─┘└───────────────┘└─────┘ └────┘└─┘
doc └─┘ └─────┘ └────┘
txt └─┘ └─────┘ └────┘
par └─┘ └─────┘ └────┘
pid ┴ └─────┘ ┴
st └─────────────────────────────────────┘
669 Exists.dcases_on hy₁' $ λ r₁ hy₁'',
id └──────────────┘ └──┘ └┘ └───┘
src └──────────────┘
typ └──────────────┘ └──┘ └┘ └───┘
670 have hyr : _ := by rw [not_imp, ←abs_lt, not_lt, abs_of_pos hy₂] at hy₁''; exact hy₁'',
id └─────┘ └────┘ └────┘ └────────┘ └─┘ └───┘
src └──┘└─────┘└─┘└────┘└┘└────┘└┘└────────┘┴ └────────┘ └────┘
typ └──┘└─────┘└─┘└────┘└┘└────┘└┘└────────┘┴└─┘└────────┘ └────┘└───┘
doc └──┘ └─┘ └┘ └┘ ┴ └────────┘ └────┘
txt └──┘ └─┘ └┘ └┘ ┴ └────────┘ └────┘
par └──┘ └─┘ └┘ └┘ ┴ └────────┘ └────┘
pid └┘ └─┘ └┘ └┘ ┴ ┴└───────┘ ┴
st └──────────┘└───────┘└──────┘└──────────────┘┴└────────────────────┘
671 by rw [←div_mul_cancel r (ne_of_gt hyr.1), ←of_eq_coe, of_mul];
id └────────────┘ ┴ └──────┘ └─┘ └───────┘ └────┘
src └───┘└────────────┘┴ ┴ └──────┘┴ └────┘└───────┘└┘└────┘┴
typ └───┘└────────────┘┴┴┴ └──────┘┴└─┘└────┘└───────┘└┘└────┘┴
doc └───┘ ┴ ┴ ┴ └────┘ └┘ ┴
txt └───┘ ┴ ┴ ┴ └────┘ └┘ ┴
par └───┘ ┴ ┴ ┴ └────┘ └┘ ┴
pid └─┘ ┴ ┴ ┴ └────┘ └┘ ┴
st └─────────────────────────────────────┘└──────────┘└──────┘┴└─
672 exact mul_lt_mul (hx (r / r₁)) hyr.2 (of_lt_of_lt U hyr.1) (le_of_lt (hx 0))
id └────────┘ ┴ ┴ └┘ └─────────┘ ┴ └─┘ └──────┘ └┘
src └────┘└────────┘┴ ┴ ┴┴┴ └─┘ └─┘ └─────────┘┴┴┴ └──┘ └──────┘┴ └────
typ └────┘└────────┘┴ ┴ ┴┴┴┴└┘└─┘ └─┘ └─────────┘┴┴┴└─┘└──┘ └──────┘┴ └┘└────
doc └────┘ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └──┘ ┴ └────
txt └────┘ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └──┘ ┴ └────
par └────┘ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └──┘ ┴ └────
pid ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └──┘ ┴ └──┘└
st ─────────────────────────────────────────────────────────────────────────────
673
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
674 lemma infinite_pos_mul_of_not_infinitesimal_pos_infinite_pos {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
675 ¬ infinitesimal x → 0 < x → infinite_pos y → infinite_pos (x * y) :=
id ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src ┴ └───────────┘ ┴ └──────────┘ └──────────┘ ┴
typ ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └───────────┘ └──────────┘ └──────────┘
676 λ hx hp hy, by rw mul_comm; exact infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos hy hx hp
id └┘ └┘ └┘ └──────┘ └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src └─┘└──────┘ └────┘└────────────────────────────────────────────────────┘┴ ┴ ┴ └
typ └┘ └┘ └┘ └─┘└──────┘ └────┘└────────────────────────────────────────────────────┘┴└┘┴└┘┴└┘└
doc └─┘ └────┘ ┴ ┴ ┴ └
txt └─┘ └────┘ ┴ ┴ ┴ └
par └─┘ └────┘ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ ┴ └
st └───────────────────────────────────────────────────────────────────────────────────
677
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
678 lemma infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
679 infinite_neg x → ¬ infinitesimal y → y < 0 → infinite_pos (x * y) :=
id └──────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴ └───────────┘ ┴ └──────────┘ ┴
typ └──────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └───────────┘ └──────────┘
680 by rw [infinite_neg_iff_infinite_pos_neg, ←neg_pos, ←neg_mul_neg, infinitesimal_neg_iff];
id └───────────────────────────────┘ └─────┘ └─────────┘ └───────────────────┘
src └──┘└───────────────────────────────┘└─┘└─────┘└─┘└─────────┘└┘└───────────────────┘┴
typ └──┘└───────────────────────────────┘└─┘└─────┘└─┘└─────────┘└┘└───────────────────┘┴
doc └──┘ └─┘ └─┘ └┘ ┴
txt └──┘ └─┘ └─┘ └┘ ┴
par └──┘ └─┘ └─┘ └┘ ┴
pid └┘ └─┘ └─┘ └┘ ┴
st └────────────────────────────────────┘└────────┘└────────────┘└─────────────────────┘┴└─
681 exact infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos
id └────────────────────────────────────────────────────┘
src └────┘└────────────────────────────────────────────────────┘└
typ └────┘└────────────────────────────────────────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ─────────────────────────────────────────────────────────────
682
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
683 lemma infinite_pos_mul_of_not_infinitesimal_neg_infinite_neg {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
684 ¬ infinitesimal x → x < 0 → infinite_neg y → infinite_pos (x * y) :=
id ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src ┴ └───────────┘ ┴ └──────────┘ └──────────┘ ┴
typ ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └───────────┘ └──────────┘ └──────────┘
685 λ hx hp hy, by rw mul_comm; exact infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg hy hx hp
id └┘ └┘ └┘ └──────┘ └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src └─┘└──────┘ └────┘└────────────────────────────────────────────────────┘┴ ┴ ┴ └
typ └┘ └┘ └┘ └─┘└──────┘ └────┘└────────────────────────────────────────────────────┘┴└┘┴└┘┴└┘└
doc └─┘ └────┘ ┴ ┴ ┴ └
txt └─┘ └────┘ ┴ ┴ ┴ └
par └─┘ └────┘ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ ┴ └
st └───────────────────────────────────────────────────────────────────────────────────
686
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
687 lemma infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
688 infinite_pos x → ¬ infinitesimal y → y < 0 → infinite_neg (x * y) :=
id └──────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴ └───────────┘ ┴ └──────────┘ ┴
typ └──────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └───────────┘ └──────────┘
689 by rw [infinite_neg_iff_infinite_pos_neg, ←neg_pos, neg_mul_eq_mul_neg, infinitesimal_neg_iff];
id └───────────────────────────────┘ └─────┘ └────────────────┘ └───────────────────┘
src └──┘└───────────────────────────────┘└─┘└─────┘└┘└────────────────┘└┘└───────────────────┘┴
typ └──┘└───────────────────────────────┘└─┘└─────┘└┘└────────────────┘└┘└───────────────────┘┴
doc └──┘ └─┘ └┘ └┘ ┴
txt └──┘ └─┘ └┘ └┘ ┴
par └──┘ └─┘ └┘ └┘ ┴
pid └┘ └─┘ └┘ └┘ ┴
st └────────────────────────────────────┘└────────┘└──────────────────┘└─────────────────────┘┴└─
690 exact infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos
id └────────────────────────────────────────────────────┘
src └────┘└────────────────────────────────────────────────────┘└
typ └────┘└────────────────────────────────────────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ─────────────────────────────────────────────────────────────
691
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
692 lemma infinite_neg_mul_of_not_infinitesimal_neg_infinite_pos {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
693 ¬ infinitesimal x → x < 0 → infinite_pos y → infinite_neg (x * y) :=
id ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src ┴ └───────────┘ ┴ └──────────┘ └──────────┘ ┴
typ ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └───────────┘ └──────────┘ └──────────┘
694 λ hx hp hy, by rw mul_comm; exact infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg hy hx hp
id └┘ └┘ └┘ └──────┘ └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src └─┘└──────┘ └────┘└────────────────────────────────────────────────────┘┴ ┴ ┴ └
typ └┘ └┘ └┘ └─┘└──────┘ └────┘└────────────────────────────────────────────────────┘┴└┘┴└┘┴└┘└
doc └─┘ └────┘ ┴ ┴ ┴ └
txt └─┘ └────┘ ┴ ┴ ┴ └
par └─┘ └────┘ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ ┴ └
st └───────────────────────────────────────────────────────────────────────────────────
695
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
696 lemma infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
697 infinite_neg x → ¬ infinitesimal y → 0 < y → infinite_neg (x * y) :=
id └──────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴ └───────────┘ ┴ └──────────┘ ┴
typ └──────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └───────────┘ └──────────┘
698 by rw [infinite_neg_iff_infinite_pos_neg, infinite_neg_iff_infinite_pos_neg, neg_mul_eq_neg_mul];
id └───────────────────────────────┘ └───────────────────────────────┘ └────────────────┘
src └──┘└───────────────────────────────┘└┘└───────────────────────────────┘└┘└────────────────┘┴
typ └──┘└───────────────────────────────┘└┘└───────────────────────────────┘└┘└────────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └────────────────────────────────────┘└─────────────────────────────────┘└──────────────────┘┴└─
699 exact infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos
id └────────────────────────────────────────────────────┘
src └────┘└────────────────────────────────────────────────────┘└
typ └────┘└────────────────────────────────────────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ─────────────────────────────────────────────────────────────
700
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
701 lemma infinite_neg_mul_of_not_infinitesimal_pos_infinite_neg {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
702 ¬ infinitesimal x → x > 0 → infinite_neg y → infinite_neg (x * y) :=
id ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src ┴ └───────────┘ ┴ └──────────┘ └──────────┘ ┴
typ ┴ └───────────┘ ┴ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └───────────┘ └──────────┘ └──────────┘
703 λ hx hp hy, by rw mul_comm; exact infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos hy hx hp
id └┘ └┘ └┘ └──────┘ └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src └─┘└──────┘ └────┘└────────────────────────────────────────────────────┘┴ ┴ ┴ └
typ └┘ └┘ └┘ └─┘└──────┘ └────┘└────────────────────────────────────────────────────┘┴└┘┴└┘┴└┘└
doc └─┘ └────┘ ┴ ┴ ┴ └
txt └─┘ └────┘ ┴ ┴ ┴ └
par └─┘ └────┘ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ ┴ └
st └───────────────────────────────────────────────────────────────────────────────────
704
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
705 lemma infinite_pos_mul_infinite_pos {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
706 infinite_pos x → infinite_pos y → infinite_pos (x * y) :=
id └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ └──────────┘ └──────────┘ ┴
typ └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘ └──────────┘
707 λ hx hy, infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos
id └┘ └┘ └────────────────────────────────────────────────────┘
src └────────────────────────────────────────────────────┘
typ └┘ └┘ └────────────────────────────────────────────────────┘
708 hx (not_infinitesimal_of_infinite_pos hy) (hy 0)
id └┘ └───────────────────────────────┘ └┘ └┘
src └───────────────────────────────┘
typ └┘ └───────────────────────────────┘ └┘ └┘
709
710 lemma infinite_neg_mul_infinite_neg {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
711 infinite_neg x → infinite_neg y → infinite_pos (x * y) :=
id └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ └──────────┘ └──────────┘ ┴
typ └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘ └──────────┘
712 λ hx hy, infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg
id └┘ └┘ └────────────────────────────────────────────────────┘
src └────────────────────────────────────────────────────┘
typ └┘ └┘ └────────────────────────────────────────────────────┘
713 hx (not_infinitesimal_of_infinite_neg hy) (hy 0)
id └┘ └───────────────────────────────┘ └┘ └┘
src └───────────────────────────────┘
typ └┘ └───────────────────────────────┘ └┘ └┘
714
715 lemma infinite_pos_mul_infinite_neg {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
716 infinite_pos x → infinite_neg y → infinite_neg (x * y) :=
id └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ └──────────┘ └──────────┘ ┴
typ └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘ └──────────┘
717 λ hx hy, infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg
id └┘ └┘ └────────────────────────────────────────────────────┘
src └────────────────────────────────────────────────────┘
typ └┘ └┘ └────────────────────────────────────────────────────┘
718 hx (not_infinitesimal_of_infinite_neg hy) (hy 0)
id └┘ └───────────────────────────────┘ └┘ └┘
src └───────────────────────────────┘
typ └┘ └───────────────────────────────┘ └┘ └┘
719
720 lemma infinite_neg_mul_infinite_pos {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
721 infinite_neg x → infinite_pos y → infinite_neg (x * y) :=
id └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ └──────────┘ └──────────┘ ┴
typ └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘ └──────────┘
722 λ hx hy, infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos
id └┘ └┘ └────────────────────────────────────────────────────┘
src └────────────────────────────────────────────────────┘
typ └┘ └┘ └────────────────────────────────────────────────────┘
723 hx (not_infinitesimal_of_infinite_pos hy) (hy 0)
id └┘ └───────────────────────────────┘ └┘ └┘
src └───────────────────────────────┘
typ └┘ └───────────────────────────────┘ └┘ └┘
724
725 lemma infinite_mul_of_infinite_not_infinitesimal {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
726 infinite x → ¬ infinitesimal y → infinite (x * y) :=
id └──────┘ ┴ ┴ └───────────┘ ┴ └──────┘ ┴ ┴ ┴
src └──────┘ ┴ └───────────┘ └──────┘ ┴
typ └──────┘ ┴ ┴ └───────────┘ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘ └───────────┘ └──────┘
727 λ hx hy, have h0 : y < 0 ∨ y > 0 := lt_or_gt_of_ne (λ H0, hy (eq.substr H0 (is_st_refl_real 0))),
id └┘ └┘ ┴ ┴ ┴ ┴ ┴ └────────────┘ └┘ └┘ └───────┘ └┘ └─────────────┘
src ┴ ┴ ┴ └────────────┘ └───────┘ └─────────────┘
typ └┘ └┘ ┴ ┴ ┴ ┴ ┴ └────────────┘ └┘ └┘ └───────┘ └┘ └─────────────┘
728 or.dcases_on hx
id └──────────┘ └┘
src └──────────┘
typ └──────────┘ └┘
729 (or.dcases_on h0
id └──────────┘ └┘
src └──────────┘
typ └──────────┘ └┘
730 (λ H0 Hx, or.inr (infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg Hx hy H0))
id └┘ └┘ └────┘ └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src └────┘ └────────────────────────────────────────────────────┘
typ └┘ └┘ └────┘ └────────────────────────────────────────────────────┘ └┘ └┘ └┘
731 (λ H0 Hx, or.inl (infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos Hx hy H0)))
id └┘ └┘ └────┘ └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src └────┘ └────────────────────────────────────────────────────┘
typ └┘ └┘ └────┘ └────────────────────────────────────────────────────┘ └┘ └┘ └┘
732 (or.dcases_on h0
id └──────────┘ └┘
src └──────────┘
typ └──────────┘ └┘
733 (λ H0 Hx, or.inl (infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg Hx hy H0))
id └┘ └┘ └────┘ └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src └────┘ └────────────────────────────────────────────────────┘
typ └┘ └┘ └────┘ └────────────────────────────────────────────────────┘ └┘ └┘ └┘
734 (λ H0 Hx, or.inr (infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos Hx hy H0)))
id └┘ └┘ └────┘ └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src └────┘ └────────────────────────────────────────────────────┘
typ └┘ └┘ └────┘ └────────────────────────────────────────────────────┘ └┘ └┘ └┘
735
736 lemma infinite_mul_of_not_infinitesimal_infinite {x y : ℝ*} :
id └┘
src └┘
typ └┘
doc └┘
737 ¬ infinitesimal x → infinite y → infinite (x * y) :=
id ┴ └───────────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴
src ┴ └───────────┘ └──────┘ └──────┘ ┴
typ ┴ └───────────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴
doc └───────────┘ └──────┘ └──────┘
738 λ hx hy, by rw [mul_comm]; exact infinite_mul_of_infinite_not_infinitesimal hy hx
id └┘ └┘ └──────┘ └────────────────────────────────────────┘ └┘ └┘
src └──┘└──────┘┴ └────┘└────────────────────────────────────────┘┴ ┴ └
typ └┘ └┘ └──┘└──────┘┴ └────┘└────────────────────────────────────────┘┴└┘┴└┘└
doc └──┘ ┴ └────┘ ┴ ┴ └
txt └──┘ ┴ └────┘ ┴ ┴ └
par └──┘ ┴ └────┘ ┴ ┴ └
pid └┘ ┴ ┴ ┴ ┴ └
st └───────────┘┴└────────────────────────────────────────────────────────
739
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
740 lemma infinite_mul_infinite {x y : ℝ*} : infinite x → infinite y → infinite (x * y) :=
id └┘ └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴
src └┘ └──────┘ └──────┘ └──────┘ ┴
typ └┘ └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴
doc └┘ └──────┘ └──────┘ └──────┘
741 λ hx hy, infinite_mul_of_infinite_not_infinitesimal hx (not_infinitesimal_of_infinite hy)
id └┘ └┘ └────────────────────────────────────────┘ └┘ └───────────────────────────┘ └┘
src └────────────────────────────────────────┘ └───────────────────────────┘
typ └┘ └┘ └────────────────────────────────────────┘ └┘ └───────────────────────────┘ └┘
742
743 end hyperreal